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/Tools/induct.ML
changeset 61853 fb7756087101
parent 61844 007d3b34080f
child 62913 13252110a6fe 
--- a/src/Tools/induct.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/induct.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -312,7 +312,9 @@
   Thm.mixed_attribute (fn (context, thm) =>
     let
       val thm' = g thm;
-      val context' = Data.map (f (name, Thm.trim_context thm')) context;
+      val context' =
+        if Thm.is_free_dummy thm then context
+        else Data.map (f (name, Thm.trim_context thm')) context;
     in (context', thm') end);
 
 fun del_att which =
isabelle