src/Pure/Isar/method.ML
changeset 16347 9b3265182607
parent 16145 1bb17485602f
child 16448 6c45c5416b79
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jun 09 12:03:33 2005 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jun 09 12:03:34 2005 +0200
     1.3 @@ -505,24 +505,20 @@
     1.4  structure MethodsDataArgs =
     1.5  struct
     1.6    val name = "Isar/methods";
     1.7 -  type T =
     1.8 -    {space: NameSpace.T,
     1.9 -     meths: (((src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
    1.10 +  type T = (((src -> Proof.context -> Proof.method) * string) * stamp) NameSpace.table;
    1.11  
    1.12 -  val empty = {space = NameSpace.empty, meths = Symtab.empty};
    1.13 +  val empty = NameSpace.empty_table;
    1.14    val copy = I;
    1.15    val prep_ext = I;
    1.16 -  fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
    1.17 -    {space = NameSpace.merge (space1, space2),
    1.18 -      meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
    1.19 -        error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
    1.20 +  fun merge tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    1.21 +    error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
    1.22  
    1.23 -  fun print _ {space, meths} =
    1.24 +  fun print _ meths =
    1.25      let
    1.26        fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.27          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.28      in
    1.29 -      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table space meths))]
    1.30 +      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    1.31        |> Pretty.chunks |> Pretty.writeln
    1.32      end;
    1.33  end;
    1.34 @@ -538,8 +534,7 @@
    1.35  
    1.36  fun method thy =
    1.37    let
    1.38 -    val {space, meths} = MethodsData.get thy;
    1.39 -
    1.40 +    val (space, meths) = MethodsData.get thy;
    1.41      fun meth src =
    1.42        let
    1.43          val ((raw_name, _), pos) = Args.dest_src src;
    1.44 @@ -558,13 +553,12 @@
    1.45    let
    1.46      val sg = Theory.sign_of thy;
    1.47      val new_meths = raw_meths |> map (fn (name, f, comment) =>
    1.48 -      (Sign.full_name sg name, ((f, comment), stamp ())));
    1.49 +      (name, ((f, comment), stamp ())));
    1.50  
    1.51 -    val {space, meths} = MethodsData.get thy;
    1.52 -    val space' = fold (Sign.declare_name sg) (map fst new_meths) space;
    1.53 -    val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups =>
    1.54 -      error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    1.55 -  in thy |> MethodsData.put {space = space', meths = meths'} end;
    1.56 +    fun add meths = NameSpace.extend_table (Sign.naming_of sg) (meths, new_meths)
    1.57 +      handle Symtab.DUPS dups =>
    1.58 +        error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    1.59 +  in MethodsData.map add thy end;
    1.60  
    1.61  val add_method = add_methods o Library.single;
    1.62