1.1 --- a/src/Pure/Isar/method.ML	Wed Aug 01 16:55:43 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 01 16:55:44 2007 +0200
     1.3 @@ -382,7 +382,7 @@
     1.4  
     1.5  (* method definitions *)
     1.6  
     1.7 -structure MethodsData = TheoryDataFun
     1.8 +structure Methods = TheoryDataFun
     1.9  (
    1.10    type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
    1.11    val empty = NameSpace.empty_table;
    1.12 @@ -394,7 +394,7 @@
    1.13  
    1.14  fun print_methods thy =
    1.15    let
    1.16 -    val meths = MethodsData.get thy;
    1.17 +    val meths = Methods.get thy;
    1.18      fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.19        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.20    in
    1.21 @@ -407,7 +407,7 @@
    1.22  
    1.23  fun method_i thy =
    1.24    let
    1.25 -    val meths = #2 (MethodsData.get thy);
    1.26 +    val meths = #2 (Methods.get thy);
    1.27      fun meth src =
    1.28        let val ((name, _), pos) = Args.dest_src src in
    1.29          (case Symtab.lookup meths name of
    1.30 @@ -416,7 +416,7 @@
    1.31        end;
    1.32    in meth end;
    1.33  
    1.34 -fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (MethodsData.get thy)));
    1.35 +fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
    1.36  
    1.37  
    1.38  (* add method *)
    1.39 @@ -428,7 +428,7 @@
    1.40  
    1.41      fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
    1.42        handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
    1.43 -  in MethodsData.map add thy end;
    1.44 +  in Methods.map add thy end;
    1.45  
    1.46  val add_method = add_methods o Library.single;
    1.47