aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
authorJosh Chen2019-02-10 10:55:37 +0100
committerJosh Chen2019-02-10 10:55:37 +0100
commit91dc4798571fa99d68ced7ba098c958fca94c477 (patch)
tree7722da549c85f3dc8ee790f6f98b70cc8d74177b /Prod.thy
parent923cfeea84cdc4292d38925e2cf6aaf07301db9c (diff)
restructure library
Diffstat (limited to '')
-rw-r--r--Prod.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Prod.thy b/Prod.thy
index ed03be5..05eff43 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -79,7 +79,7 @@ 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 ctxt)
+ val [g, f] = [g, f] |> map (Util.prep_term ctxt)
val dom =
case f of
Const ("Prod.lam", _) $ T $ _ => T