--- a/src/HOL/Import/hol4rews.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Jun 17 18:33:05 2005 +0200
@@ -18,9 +18,9 @@
type T = ImportStatus
val empty = NoImport
val copy = I
-val prep_ext = I
-fun merge (NoImport,NoImport) = NoImport
- | merge _ = (warning "Import status set during merge"; NoImport)
+val extend = I
+fun merge _ (NoImport,NoImport) = NoImport
+ | merge _ _ = (warning "Import status set during merge"; NoImport)
fun print sg import_status =
Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
end;
@@ -33,10 +33,10 @@
type T = string
val empty = ""
val copy = I
-val prep_ext = I
-fun merge ("",arg) = arg
- | merge (arg,"") = arg
- | merge (s1,s2) =
+val extend = I
+fun merge _ ("",arg) = arg
+ | merge _ (arg,"") = arg
+ | merge _ (s1,s2) =
if s1 = s2
then s1
else error "Trying to merge two different import segments"
@@ -55,9 +55,9 @@
type T = string list
val empty = []
val copy = I
-val prep_ext = I
-fun merge ([],[]) = []
- | merge _ = error "Used names not empty during merge"
+val extend = I
+fun merge _ ([],[]) = []
+ | merge _ _ = error "Used names not empty during merge"
fun print sg used_names =
Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
end;
@@ -70,9 +70,9 @@
type T = string * string * string list
val empty = ("","",[])
val copy = I
-val prep_ext = I
-fun merge (("","",[]),("","",[])) = ("","",[])
- | merge _ = error "Dump data not empty during merge"
+val extend = I
+fun merge _ (("","",[]),("","",[])) = ("","",[])
+ | merge _ _ = error "Dump data not empty during merge"
fun print sg dump_data =
Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
end;
@@ -85,8 +85,8 @@
type T = string Symtab.table
val empty = Symtab.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = Symtab.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = Symtab.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 moves:"
(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
@@ -100,8 +100,8 @@
type T = string Symtab.table
val empty = Symtab.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = Symtab.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = Symtab.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 imports:"
(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
@@ -130,8 +130,8 @@
type T = string Symtab.table
val empty = Symtab.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = Symtab.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = Symtab.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
@@ -145,8 +145,8 @@
type T = (string option) StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 mappings:"
(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab)))
@@ -160,8 +160,8 @@
type T = holthm StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 mappings:"
(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
@@ -175,8 +175,8 @@
type T = (bool * string * typ option) StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
@@ -190,8 +190,8 @@
type T = string StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
@@ -205,8 +205,8 @@
type T = string StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
@@ -220,8 +220,8 @@
type T = (bool * string) StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
@@ -235,8 +235,8 @@
type T = ((term * term) list * thm) StringPair.table
val empty = StringPair.empty
val copy = I
-val prep_ext = I
-val merge : T * T -> T = StringPair.merge (K true)
+val extend = I
+fun merge _ : T * T -> T = StringPair.merge (K true)
fun print sg tab =
Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
@@ -250,8 +250,8 @@
type T = thm list
val empty = []
val copy = I
-val prep_ext = I
-val merge = Library.gen_union Thm.eq_thm
+val extend = I
+fun merge _ = Library.gen_union Thm.eq_thm
fun print sg thms =
Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
(map Display.pretty_thm thms))
@@ -480,7 +480,7 @@
fun process (thy,((bthy,bthm),hth as (_,thm))) =
let
val sg = sign_of thy
- val thm1 = rewrite_rule (map (transfer_sg sg) rews) (transfer_sg sg thm)
+ val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm)
val thm2 = standard thm1
val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy
val thy5 = add_hol4_theorem bthy bthm hth thy2
--- a/src/HOL/Import/import_package.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Import/import_package.ML Fri Jun 17 18:33:05 2005 +0200
@@ -16,10 +16,9 @@
type T = ProofKernel.thm option array option
val empty = NONE
val copy = I
-val prep_ext = I
-fun merge _ = NONE
-fun print sg import_segment =
- Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented"))
+val extend = I
+fun merge _ _ = NONE
+fun print _ _ = ()
end
structure ImportData = TheoryDataFun(ImportDataArgs)
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Jun 17 18:33:05 2005 +0200
@@ -18,8 +18,8 @@
(**** theory data ****)
-structure CodegenArgs =
-struct
+structure CodegenData = TheoryDataFun
+(struct
val name = "HOL/inductive_codegen";
type T =
{intros : thm list Symtab.table,
@@ -28,16 +28,15 @@
val empty =
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
val copy = I;
- val prep_ext = I;
- fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
+ val extend = I;
+ fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
{intros=intros2, graph=graph2, eqns=eqns2}) =
{intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
fun print _ _ = ();
-end;
+end);
-structure CodegenData = TheoryDataFun(CodegenArgs);
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
string_of_thm thm);
--- a/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:05 2005 +0200
@@ -16,18 +16,17 @@
open Codegen;
-structure CodegenArgs =
-struct
+structure CodegenData = TheoryDataFun
+(struct
val name = "HOL/recfun_codegen";
type T = thm list Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- val merge = Symtab.merge_multi' Drule.eq_thm_prop;
+ val extend = I;
+ fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
fun print _ _ = ();
-end;
+end);
-structure CodegenData = TheoryDataFun(CodegenArgs);
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
val lhs_of = fst o dest_eqn o prop_of;
--- a/src/HOL/Tools/refute.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/Tools/refute.ML Fri Jun 17 18:33:05 2005 +0200
@@ -183,8 +183,8 @@
parameters: string Symtab.table};
val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
val copy = I;
- val prep_ext = I;
- fun merge
+ val extend = I;
+ fun merge _
({interpreters = in1, printers = pr1, parameters = pa1},
{interpreters = in2, printers = pr2, parameters = pa2}) =
{interpreters = rev (merge_alists (rev in1) (rev in2)),
--- a/src/HOL/arith_data.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/HOL/arith_data.ML Fri Jun 17 18:33:05 2005 +0200
@@ -201,24 +201,22 @@
(* arith theory data *)
-structure ArithTheoryDataArgs =
-struct
+structure ArithTheoryData = TheoryDataFun
+(struct
val name = "HOL/arith";
type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int -> tactic) option};
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
val copy = I;
- val prep_ext = I;
- fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
+ val extend = I;
+ fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
{splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
{splits = Drule.merge_rules (splits1, splits2),
inj_consts = merge_lists inj_consts1 inj_consts2,
discrete = merge_lists discrete1 discrete2,
presburger = (case presburger1 of NONE => presburger2 | p => p)};
fun print _ _ = ();
-end;
-
-structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
+end);
fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
{splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
@@ -360,7 +358,7 @@
| decomp2 data _ = NONE
fun decomp sg =
- let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
+ let val {discrete, inj_consts, ...} = ArithTheoryData.get sg
in decomp2 (sg,discrete,inj_consts) end
fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
@@ -458,12 +456,12 @@
fun raw_arith_tac ex i st =
refute_tac (K true)
- (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
+ (REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.sign_of_thm st))))
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
i st;
fun presburger_tac i st =
- (case ArithTheoryData.get_sg (sign_of_thm st) of
+ (case ArithTheoryData.get (sign_of_thm st) of
{presburger = SOME tac, ...} =>
(tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
| _ => no_tac st);
--- a/src/Provers/classical.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Provers/classical.ML Fri Jun 17 18:33:05 2005 +0200
@@ -79,10 +79,10 @@
val appSWrappers : claset -> wrapper
val appWrappers : claset -> wrapper
- val claset_ref_of_sg: Sign.sg -> claset ref
val claset_ref_of: theory -> claset ref
- val claset_of_sg: Sign.sg -> claset
+ val claset_ref_of_sg: theory -> claset ref (*obsolete*)
val claset_of: theory -> claset
+ val claset_of_sg: theory -> claset (*obsolete*)
val CLASET: (claset -> tactic) -> tactic
val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
val claset: unit -> claset
@@ -826,23 +826,22 @@
(* theory data kind 'Provers/claset' *)
-structure GlobalClasetArgs =
-struct
+structure GlobalClaset = TheoryDataFun
+(struct
val name = "Provers/claset";
type T = claset ref * context_cs;
val empty = (ref empty_cs, empty_context_cs);
- fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; (*create new reference!*)
- val prep_ext = copy;
- fun merge ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
+ fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
+ val extend = copy;
+ fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
(ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
fun print _ (ref cs, _) = print_cs cs;
-end;
+end);
-structure GlobalClaset = TheoryDataFun(GlobalClasetArgs);
val print_claset = GlobalClaset.print;
-val claset_ref_of_sg = #1 o GlobalClaset.get_sg;
val claset_ref_of = #1 o GlobalClaset.get;
+val claset_ref_of_sg = claset_ref_of;
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
fun map_context_cs f = GlobalClaset.map (apsnd
@@ -851,14 +850,14 @@
(* access claset *)
-val claset_of_sg = ! o claset_ref_of_sg;
-val claset_of = claset_of_sg o Theory.sign_of;
+val claset_of = ! o claset_ref_of;
+val claset_of_sg = claset_of;
-fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
-fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
+fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state;
+fun CLASET' tacf i state = tacf (claset_of (Thm.theory_of_thm state)) i state;
val claset = claset_of o Context.the_context;
-val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
+val claset_ref = claset_ref_of o Context.the_context;
(* change claset *)
@@ -885,15 +884,14 @@
(* proof data kind 'Provers/claset' *)
-structure LocalClasetArgs =
-struct
+structure LocalClaset = ProofDataFun
+(struct
val name = "Provers/claset";
type T = claset;
val init = claset_of;
fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
-end;
+end);
-structure LocalClaset = ProofDataFun(LocalClasetArgs);
val print_local_claset = LocalClaset.print;
val get_local_claset = LocalClaset.get;
val put_local_claset = LocalClaset.put;
@@ -921,7 +919,7 @@
in (ctxt', #2 (DeltaClasetData.get ctxt'))
end;
-local
+local
fun rename_thm' (ctxt,thm) =
let val (new_ctxt, new_id) = delta_increment ctxt
val new_name = "anon_cla_" ^ (string_of_int new_id)
@@ -935,7 +933,7 @@
fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
end
-
+
(* attributes *)
@@ -961,60 +959,60 @@
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addSDs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
+ val new_dcs = delta_cs addSDs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
in
- change_local_cs (op addSDs) (ctxt'',th)
+ change_local_cs (op addSDs) (ctxt'',th)
end;
-fun safe_elim_local (ctxt, th)=
+fun safe_elim_local (ctxt, th)=
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addSEs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
+ val new_dcs = delta_cs addSEs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
in
- change_local_cs (op addSEs) (ctxt'',th)
+ change_local_cs (op addSEs) (ctxt'',th)
end;
-fun safe_intro_local (ctxt, th) =
+fun safe_intro_local (ctxt, th) =
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addSIs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
+ val new_dcs = delta_cs addSIs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
in
- change_local_cs (op addSIs) (ctxt'',th)
+ change_local_cs (op addSIs) (ctxt'',th)
end;
-fun haz_dest_local (ctxt, th)=
+fun haz_dest_local (ctxt, th)=
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addDs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
+ val new_dcs = delta_cs addDs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
in
- change_local_cs (op addDs) (ctxt'',th)
+ change_local_cs (op addDs) (ctxt'',th)
end;
fun haz_elim_local (ctxt,th) =
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addEs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
- in
- change_local_cs (op addEs) (ctxt'',th)
+ val new_dcs = delta_cs addEs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
+ in
+ change_local_cs (op addEs) (ctxt'',th)
end;
-fun haz_intro_local (ctxt,th) =
+fun haz_intro_local (ctxt,th) =
let val thm_name = Thm.name_of_thm th
val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
val delta_cs = get_delta_claset ctxt'
- val new_dcs = delta_cs addIs [th']
- val ctxt'' = put_delta_claset new_dcs ctxt'
- in
- change_local_cs (op addIs) (ctxt'',th)
+ val new_dcs = delta_cs addIs [th']
+ val ctxt'' = put_delta_claset new_dcs ctxt'
+ in
+ change_local_cs (op addIs) (ctxt'',th)
end;
--- a/src/Pure/Isar/calculation.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Jun 17 18:33:05 2005 +0200
@@ -32,43 +32,41 @@
(** global and local calculation data **)
-(* theory data kind 'Isar/calculation' *)
+(* global calculation *)
fun print_rules prt x (trans, sym) =
[Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
Pretty.big_list "symmetry rules:" (map (prt x) sym)]
|> Pretty.chunks |> Pretty.writeln;
-structure GlobalCalculationArgs =
-struct
+structure GlobalCalculation = TheoryDataFun
+(struct
val name = "Isar/calculation";
type T = thm NetRules.T * thm list
val empty = (NetRules.elim, []);
val copy = I;
- val prep_ext = I;
- fun merge ((trans1, sym1), (trans2, sym2)) =
+ val extend = I;
+ fun merge _ ((trans1, sym1), (trans2, sym2)) =
(NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
val print = print_rules Display.pretty_thm_sg;
-end;
+end);
-structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
val _ = Context.add_setup [GlobalCalculation.init];
val print_global_rules = GlobalCalculation.print;
-(* proof data kind 'Isar/calculation' *)
+(* local calculation *)
-structure LocalCalculationArgs =
-struct
+structure LocalCalculation = ProofDataFun
+(struct
val name = "Isar/calculation";
type T = (thm NetRules.T * thm list) * (thm list * int) option;
fun init thy = (GlobalCalculation.get thy, NONE);
fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
-end;
+end);
-structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
val _ = Context.add_setup [LocalCalculation.init];
val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
val print_local_rules = LocalCalculation.print;
--- a/src/Pure/Isar/context_rules.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Jun 17 18:33:05 2005 +0200
@@ -126,9 +126,9 @@
val empty = make_rules ~1 [] empty_netpairs ([], []);
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
+ fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
@@ -147,15 +147,14 @@
val _ = Context.add_setup [GlobalRules.init];
val print_global_rules = GlobalRules.print;
-structure LocalRulesArgs =
-struct
+structure LocalRules = ProofDataFun
+(struct
val name = GlobalRulesArgs.name;
type T = GlobalRulesArgs.T;
val init = GlobalRules.get;
val print = print_rules ProofContext.pretty_thm;
-end;
+end);
-structure LocalRules = ProofDataFun(LocalRulesArgs);
val _ = Context.add_setup [LocalRules.init];
val print_local_rules = LocalRules.print;
@@ -175,22 +174,25 @@
if k = k' then untaglist rest
else x :: untaglist rest;
-fun orderlist brls =
- untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
-fun orderlist_no_weight brls =
- untaglist (sort (Int.compare o pairself (snd o fst)) brls);
+fun orderlist brls =
+ untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
+
+fun orderlist_no_weight brls =
+ untaglist (sort (Int.compare o pairself (snd o fst)) brls);
fun may_unify weighted t net =
map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
fun find_erules _ [] = K []
| find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact));
+
fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
fun find_rules_netpair weighted facts goal (inet, enet) =
find_erules weighted facts enet @ find_irules weighted goal inet;
-fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
+fun find_rules weighted facts goals =
+ map (find_rules_netpair weighted facts goals) o netpairs;
(* wrappers *)
@@ -268,5 +270,4 @@
val addXDs_local = modifier (dest_query_local NONE);
val delrules_local = modifier rule_del_local;
-
end;
--- a/src/Pure/Isar/induct_attrib.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Pure/Isar/induct_attrib.ML Fri Jun 17 18:33:05 2005 +0200
@@ -85,7 +85,7 @@
NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
Drule.eq_thm_prop (th1, th2));
-fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
+fun lookup_rule (rs: rules) name = assoc_string (NetRules.rules rs, name);
fun print_rules prt kind x rs =
let val thms = map snd (NetRules.rules rs)
@@ -109,8 +109,8 @@
((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
val copy = I;
- val prep_ext = I;
- fun merge (((casesT1, casesS1), (inductT1, inductS1)),
+ val extend = I;
+ fun merge _ (((casesT1, casesS1), (inductT1, inductS1)),
((casesT2, casesS2), (inductT2, inductS2))) =
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
@@ -132,16 +132,15 @@
(* proof data kind 'Isar/induction' *)
-structure LocalInductArgs =
-struct
+structure LocalInduct = ProofDataFun
+(struct
val name = "Isar/induction";
type T = GlobalInductArgs.T;
fun init thy = GlobalInduct.get thy;
fun print x = print_all_rules ProofContext.pretty_thm x;
-end;
+end);
-structure LocalInduct = ProofDataFun(LocalInductArgs);
val _ = Context.add_setup [LocalInduct.init];
val print_local_rules = LocalInduct.print;
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
@@ -229,5 +228,4 @@
[(casesN, cases_attr, "declaration of cases rule for type or set"),
(inductN, induct_attr, "declaration of induction rule for type or set")]];
-
end;
--- a/src/Pure/Isar/term_style.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/Pure/Isar/term_style.ML Fri Jun 17 18:33:05 2005 +0200
@@ -20,19 +20,18 @@
fun err_dup_styles names =
error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
-structure StyleArgs =
-struct
+structure StyleData = TheoryDataFun
+(struct
val name = "Isar/style";
type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- fun merge tabs = Symtab.merge eq_snd tabs
+ val extend = I;
+ fun merge _ tabs = Symtab.merge eq_snd tabs
handle Symtab.DUPS dups => err_dup_styles dups;
fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
-end;
+end);
-structure StyleData = TheoryDataFun(StyleArgs);
val _ = Context.add_setup [StyleData.init];
val print_styles = StyleData.print;
@@ -52,16 +51,19 @@
(* predefined styles *)
fun style_binargs ctxt t =
- let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
+ let
+ val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
+ (Logic.strip_imp_concl t)
+ in
case concl of (_ $ l $ r) => (l, r)
| _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
end;
fun style_parm_premise i ctxt t =
- let val prems = Logic.strip_imp_prems t
- in if i <= length prems then List.nth(prems, i-1)
- else error ("Not enough premises for prem" ^ string_of_int i ^
- " in propositon: " ^ ProofContext.string_of_term ctxt t)
+ let val prems = Logic.strip_imp_prems t in
+ if i <= length prems then List.nth (prems, i - 1)
+ else error ("Not enough premises for prem" ^ string_of_int i ^
+ " in propositon: " ^ ProofContext.string_of_term ctxt t)
end;
val _ = Context.add_setup
--- a/src/ZF/Tools/ind_cases.ML Fri Jun 17 18:33:03 2005 +0200
+++ b/src/ZF/Tools/ind_cases.ML Fri Jun 17 18:33:05 2005 +0200
@@ -18,19 +18,18 @@
(* theory data *)
-structure IndCasesArgs =
-struct
+structure IndCasesData = TheoryDataFun
+(struct
val name = "ZF/ind_cases";
type T = (simpset -> cterm -> thm) Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
+ val extend = I;
+ fun merge _ tabs : T = Symtab.merge (K true) tabs;
fun print _ _ = ();
-end;
+end);
-structure IndCasesData = TheoryDataFun(IndCasesArgs);
fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab));