src/Pure/Isar/locale.ML
changeset 30223 24d975352879
parent 29576 669b560fc2b9
child 30344 10a67c5ddddb
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Mar 03 18:31:59 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Mar 03 18:32:01 2009 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4  fun axioms_of thy = #axioms o the_locale thy;
     1.5  
     1.6  fun instance_of thy name morph = params_of thy name |>
     1.7 -  map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
     1.8 +  map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
     1.9  
    1.10  fun specification_of thy = #spec o the_locale thy;
    1.11  
    1.12 @@ -464,8 +464,7 @@
    1.13  fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
    1.14  
    1.15  fun add_decls add loc decl =
    1.16 -  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
    1.17 -    #>
    1.18 +  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
    1.19    add_thmss loc Thm.internalK
    1.20      [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
    1.21