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