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/Pure/Isar/specification.ML
changeset 32661 f4d179d91af2
parent 30763 6976521b4263
child 32662 2faf1148c062 
--- a/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -209,7 +209,8 @@
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2
       |> LocalTheory.note Thm.definitionK
-        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
+        ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts),
+          [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ =
isabelle