Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
authorwenzelm
Thu Nov 19 14:45:56 2009 +0100 (2009-11-19)
changeset 3376547b5db097646
parent 33764 7bcefaab8d41
child 33766 c679f05600cd
Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 19 14:44:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 19 14:45:56 2009 +0100
     1.3 @@ -204,8 +204,7 @@
     1.4            in (b, mx) end);
     1.5      val name = Thm.def_binding_optional b raw_name;
     1.6      val ((lhs, (_, raw_th)), lthy2) = lthy
     1.7 -      |> Local_Theory.define Thm.definitionK
     1.8 -        (var, ((Binding.suffix_name "_raw" name, []), rhs));
     1.9 +      |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
    1.10  
    1.11      val th = prove lthy2 raw_th;
    1.12      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);