Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 31 May 2015 00:16:26 +0200
changeset 60321 42079156c5aa
parent 60320 e7c0ca878120
child 60322 05fabeb0130a
tuned;
src/HOL/Tools/Function/mutual.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/mutual.ML	Sun May 31 00:11:12 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun May 31 00:16:26 2015 +0200
@@ -250,7 +250,7 @@
     val [P, x] =
       Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
       |> map (Thm.cterm_of ctxt o Free);
-    val sumtree_inj = Drule.cterm_fun (Sum_Tree.mk_inj ST n i) x;
+    val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));
 
     fun prep_subgoal_tac i =
       REPEAT (eresolve_tac ctxt
isabelle