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/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59644 cc78fd8d955d 
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -36,7 +36,7 @@
       |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
       ||> fst o split_last |> list_comb;
     val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
-    val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
+    val assum = Thm.global_cterm_of thy (Logic.mk_equals (lhs, rhs));
   in
     thms
     |> Conjunction.intr_balanced
isabelle