Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Tools/cartprod.ML
changeset 59621 291934bac95e
parent 54742 7a86358a3c0b
child 59626 a6e977d8b070 
--- a/src/ZF/Tools/cartprod.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/ZF/Tools/cartprod.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -106,7 +106,7 @@
 fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
       let val T' = factors T1 ---> T2
           val newt = ap_split T1 T2 (Var(v,T'))
-          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
+          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
       in
           remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
                                            cterm newt)]) rl)
isabelle