From 923cfeea84cdc4292d38925e2cf6aaf07301db9c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 10 Feb 2019 03:17:12 +0100
Subject: Fix antiquotation situation

---
 Prod.thy | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/Prod.thy b/Prod.thy
index ce785d6..ed03be5 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -79,15 +79,18 @@ syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "o" 110)
 parse_translation \<open>
 let fun compose_tr ctxt [g, f] =
   let
-    val [g, f] = [g, f] |> map (Typing.prep_term @{context})
+    val [g, f] = [g, f] |> map (Typing.prep_term ctxt)
     val dom =
       case f of
         Const ("Prod.lam", _) $ T $ _ => T
       | Const ("Prod.compose", _) $ T $ _ $ _ => T
-      | _ => (case Typing.get_typing ctxt f of
-               SOME (Const ("Prod.Prod", _) $ T $ _) => T
-             | SOME t => (@{print} t; Exn.error "Can't compose with a non-function")
-             | NONE => Exn.error "Cannot infer domain of composition; please state this explicitly")
+      | _ =>
+          case Typing.get_typing ctxt f of
+            SOME (Const ("Prod.Prod", _) $ T $ _) => T
+          | SOME t =>
+              Exn.error ("Can't compose with a non-function " ^ Syntax.string_of_term ctxt f)
+          | NONE =>
+              Exn.error "Cannot infer domain of composition; please state this explicitly"
   in
     @{const compose} $ dom $ g $ f
   end
-- 
cgit v1.2.3