src/HOL/Tools/recdef_package.ML
changeset 16458 4c6fd0c01d28
parent 16364 dc9f7066d80a
child 16646 666774b0d1b0
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -103,28 +103,27 @@
     1.4  
     1.5  type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
     1.6  
     1.7 -structure GlobalRecdefArgs =
     1.8 -struct
     1.9 +structure GlobalRecdefData = TheoryDataFun
    1.10 +(struct
    1.11    val name = "HOL/recdef";
    1.12    type T = recdef_info Symtab.table * hints;
    1.13  
    1.14    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
    1.15    val copy = I;
    1.16 -  val prep_ext = I;
    1.17 -  fun merge
    1.18 +  val extend = I;
    1.19 +  fun merge _
    1.20     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
    1.21 -    (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) =
    1.22 +    (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
    1.23        (Symtab.merge (K true) (tab1, tab2),
    1.24          mk_hints (Drule.merge_rules (simps1, simps2),
    1.25            Library.merge_alists congs1 congs2,
    1.26            Drule.merge_rules (wfs1, wfs2)));
    1.27  
    1.28 -  fun print sg (tab, hints) =
    1.29 -    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
    1.30 +  fun print thy (tab, hints) =
    1.31 +    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
    1.32        pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
    1.33 -end;
    1.34 +end);
    1.35  
    1.36 -structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
    1.37  val print_recdefs = GlobalRecdefData.print;
    1.38  
    1.39  
    1.40 @@ -143,15 +142,14 @@
    1.41  
    1.42  (* proof data kind 'HOL/recdef' *)
    1.43  
    1.44 -structure LocalRecdefArgs =
    1.45 -struct
    1.46 +structure LocalRecdefData = ProofDataFun
    1.47 +(struct
    1.48    val name = "HOL/recdef";
    1.49    type T = hints;
    1.50    val init = get_global_hints;
    1.51    fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
    1.52 -end;
    1.53 +end);
    1.54  
    1.55 -structure LocalRecdefData = ProofDataFun(LocalRecdefArgs);
    1.56  val get_local_hints = LocalRecdefData.get;
    1.57  val map_local_hints = LocalRecdefData.map;
    1.58  
    1.59 @@ -234,7 +232,7 @@
    1.60    let
    1.61      val _ = requires_recdef thy;
    1.62  
    1.63 -    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.64 +    val name = Sign.intern_const thy raw_name;
    1.65      val bname = Sign.base_name name;
    1.66      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.67  
    1.68 @@ -282,7 +280,7 @@
    1.69  
    1.70  fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
    1.71    let
    1.72 -    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.73 +    val name = Sign.intern_const thy raw_name;
    1.74      val bname = Sign.base_name name;
    1.75  
    1.76      val _ = requires_recdef thy;
    1.77 @@ -306,7 +304,7 @@
    1.78  
    1.79  fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int thy =
    1.80    let
    1.81 -    val name = prep_name (Theory.sign_of thy) raw_name;
    1.82 +    val name = prep_name thy raw_name;
    1.83      val atts = map (prep_att thy) raw_atts;
    1.84      val tcs =
    1.85        (case get_recdef thy name of
    1.86 @@ -380,6 +378,4 @@
    1.87  
    1.88  end;
    1.89  
    1.90 -
    1.91  end;
    1.92 -