src/Pure/Isar/specification.ML
changeset 25016 2bcac52d7abc
parent 25011 633afd909ff2
child 25211 aec1cbdbca71
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Oct 12 22:01:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Oct 13 17:16:39 2007 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4        if x = x' then mx
     1.5        else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
     1.6      val ((lhs, (_, th)), lthy2) = lthy
     1.7 -      |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     1.8 +      |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     1.9      val ((b, [th']), lthy3) = lthy2
    1.10        |> LocalTheory.note Thm.definitionK
    1.11            ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);