accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:33:05 2005 +0200 (2005-06-17 ago)
changeset 1642418a07ad8fea8
parent 16423 24abe4c0e4b4
child 16425 2427be27cc60
accomodate change of TheoryDataFun;
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/refute.ML
src/HOL/arith_data.ML
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/term_style.ML
src/ZF/Tools/ind_cases.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Fri Jun 17 18:33:05 2005 +0200
     1.3 @@ -18,9 +18,9 @@
     1.4  type T = ImportStatus
     1.5  val empty = NoImport
     1.6  val copy = I
     1.7 -val prep_ext = I
     1.8 -fun merge (NoImport,NoImport) = NoImport
     1.9 -  | merge _ = (warning "Import status set during merge"; NoImport)
    1.10 +val extend = I
    1.11 +fun merge _ (NoImport,NoImport) = NoImport
    1.12 +  | merge _ _ = (warning "Import status set during merge"; NoImport)
    1.13  fun print sg import_status =
    1.14      Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
    1.15  end;
    1.16 @@ -33,10 +33,10 @@
    1.17  type T = string
    1.18  val empty = ""
    1.19  val copy = I
    1.20 -val prep_ext = I
    1.21 -fun merge ("",arg) = arg
    1.22 -  | merge (arg,"") = arg
    1.23 -  | merge (s1,s2) =
    1.24 +val extend = I
    1.25 +fun merge _ ("",arg) = arg
    1.26 +  | merge _ (arg,"") = arg
    1.27 +  | merge _ (s1,s2) =
    1.28      if s1 = s2
    1.29      then s1
    1.30      else error "Trying to merge two different import segments"
    1.31 @@ -55,9 +55,9 @@
    1.32  type T = string list
    1.33  val empty = []
    1.34  val copy = I
    1.35 -val prep_ext = I
    1.36 -fun merge ([],[]) = []
    1.37 -  | merge _ = error "Used names not empty during merge"
    1.38 +val extend = I
    1.39 +fun merge _ ([],[]) = []
    1.40 +  | merge _ _ = error "Used names not empty during merge"
    1.41  fun print sg used_names =
    1.42      Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
    1.43  end;
    1.44 @@ -70,9 +70,9 @@
    1.45  type T = string * string * string list
    1.46  val empty = ("","",[])
    1.47  val copy = I
    1.48 -val prep_ext = I
    1.49 -fun merge (("","",[]),("","",[])) = ("","",[])
    1.50 -  | merge _ = error "Dump data not empty during merge"
    1.51 +val extend = I
    1.52 +fun merge _ (("","",[]),("","",[])) = ("","",[])
    1.53 +  | merge _ _ = error "Dump data not empty during merge"
    1.54  fun print sg dump_data =
    1.55      Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
    1.56  end;
    1.57 @@ -85,8 +85,8 @@
    1.58  type T = string Symtab.table
    1.59  val empty = Symtab.empty
    1.60  val copy = I
    1.61 -val prep_ext = I
    1.62 -val merge : T * T -> T = Symtab.merge (K true)
    1.63 +val extend = I
    1.64 +fun merge _ : T * T -> T = Symtab.merge (K true)
    1.65  fun print sg tab =
    1.66      Pretty.writeln (Pretty.big_list "HOL4 moves:"
    1.67  	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
    1.68 @@ -100,8 +100,8 @@
    1.69  type T = string Symtab.table
    1.70  val empty = Symtab.empty
    1.71  val copy = I
    1.72 -val prep_ext = I
    1.73 -val merge : T * T -> T = Symtab.merge (K true)
    1.74 +val extend = I
    1.75 +fun merge _ : T * T -> T = Symtab.merge (K true)
    1.76  fun print sg tab =
    1.77      Pretty.writeln (Pretty.big_list "HOL4 imports:"
    1.78  	(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
    1.79 @@ -130,8 +130,8 @@
    1.80  type T = string Symtab.table
    1.81  val empty = Symtab.empty
    1.82  val copy = I
    1.83 -val prep_ext = I
    1.84 -val merge : T * T -> T = Symtab.merge (K true)
    1.85 +val extend = I
    1.86 +fun merge _ : T * T -> T = Symtab.merge (K true)
    1.87  fun print sg tab =
    1.88      Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
    1.89  	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
    1.90 @@ -145,8 +145,8 @@
    1.91  type T = (string option) StringPair.table
    1.92  val empty = StringPair.empty
    1.93  val copy = I
    1.94 -val prep_ext = I
    1.95 -val merge : T * T -> T = StringPair.merge (K true)
    1.96 +val extend = I
    1.97 +fun merge _ : T * T -> T = StringPair.merge (K true)
    1.98  fun print sg tab =
    1.99      Pretty.writeln (Pretty.big_list "HOL4 mappings:"
   1.100  	(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab)))
   1.101 @@ -160,8 +160,8 @@
   1.102  type T = holthm StringPair.table
   1.103  val empty = StringPair.empty
   1.104  val copy = I
   1.105 -val prep_ext = I
   1.106 -val merge : T * T -> T = StringPair.merge (K true)
   1.107 +val extend = I
   1.108 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.109  fun print sg tab =
   1.110      Pretty.writeln (Pretty.big_list "HOL4 mappings:"
   1.111  	(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
   1.112 @@ -175,8 +175,8 @@
   1.113  type T = (bool * string * typ option) StringPair.table
   1.114  val empty = StringPair.empty
   1.115  val copy = I
   1.116 -val prep_ext = I
   1.117 -val merge : T * T -> T = StringPair.merge (K true)
   1.118 +val extend = I
   1.119 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.120  fun print sg tab =
   1.121      Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
   1.122  	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
   1.123 @@ -190,8 +190,8 @@
   1.124  type T = string StringPair.table
   1.125  val empty = StringPair.empty
   1.126  val copy = I
   1.127 -val prep_ext = I
   1.128 -val merge : T * T -> T = StringPair.merge (K true)
   1.129 +val extend = I
   1.130 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.131  fun print sg tab =
   1.132      Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
   1.133  	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
   1.134 @@ -205,8 +205,8 @@
   1.135  type T = string StringPair.table
   1.136  val empty = StringPair.empty
   1.137  val copy = I
   1.138 -val prep_ext = I
   1.139 -val merge : T * T -> T = StringPair.merge (K true)
   1.140 +val extend = I
   1.141 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.142  fun print sg tab =
   1.143      Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
   1.144  	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
   1.145 @@ -220,8 +220,8 @@
   1.146  type T = (bool * string) StringPair.table
   1.147  val empty = StringPair.empty
   1.148  val copy = I
   1.149 -val prep_ext = I
   1.150 -val merge : T * T -> T = StringPair.merge (K true)
   1.151 +val extend = I
   1.152 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.153  fun print sg tab =
   1.154      Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
   1.155  	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
   1.156 @@ -235,8 +235,8 @@
   1.157  type T = ((term * term) list * thm) StringPair.table
   1.158  val empty = StringPair.empty
   1.159  val copy = I
   1.160 -val prep_ext = I
   1.161 -val merge : T * T -> T = StringPair.merge (K true)
   1.162 +val extend = I
   1.163 +fun merge _ : T * T -> T = StringPair.merge (K true)
   1.164  fun print sg tab =
   1.165      Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
   1.166  	(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
   1.167 @@ -250,8 +250,8 @@
   1.168  type T = thm list
   1.169  val empty = []
   1.170  val copy = I
   1.171 -val prep_ext = I
   1.172 -val merge = Library.gen_union Thm.eq_thm
   1.173 +val extend = I
   1.174 +fun merge _ = Library.gen_union Thm.eq_thm
   1.175  fun print sg thms =
   1.176      Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
   1.177  				    (map Display.pretty_thm thms))
   1.178 @@ -480,7 +480,7 @@
   1.179  	fun process (thy,((bthy,bthm),hth as (_,thm))) =
   1.180  	    let
   1.181  		val sg      = sign_of thy
   1.182 -		val thm1 = rewrite_rule (map (transfer_sg sg) rews) (transfer_sg sg thm)
   1.183 +		val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm)
   1.184  		val thm2 = standard thm1
   1.185  		val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy
   1.186  		val thy5 = add_hol4_theorem bthy bthm hth thy2
     2.1 --- a/src/HOL/Import/import_package.ML	Fri Jun 17 18:33:03 2005 +0200
     2.2 +++ b/src/HOL/Import/import_package.ML	Fri Jun 17 18:33:05 2005 +0200
     2.3 @@ -16,10 +16,9 @@
     2.4  type T = ProofKernel.thm option array option
     2.5  val empty = NONE
     2.6  val copy = I
     2.7 -val prep_ext = I
     2.8 -fun merge _ = NONE
     2.9 -fun print sg import_segment =
    2.10 -    Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented"))
    2.11 +val extend = I
    2.12 +fun merge _ _ = NONE
    2.13 +fun print _ _ = ()
    2.14  end
    2.15  
    2.16  structure ImportData = TheoryDataFun(ImportDataArgs)
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jun 17 18:33:03 2005 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jun 17 18:33:05 2005 +0200
     3.3 @@ -18,8 +18,8 @@
     3.4  
     3.5  (**** theory data ****)
     3.6  
     3.7 -structure CodegenArgs =
     3.8 -struct
     3.9 +structure CodegenData = TheoryDataFun
    3.10 +(struct
    3.11    val name = "HOL/inductive_codegen";
    3.12    type T =
    3.13      {intros : thm list Symtab.table,
    3.14 @@ -28,16 +28,15 @@
    3.15    val empty =
    3.16      {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
    3.17    val copy = I;
    3.18 -  val prep_ext = I;
    3.19 -  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
    3.20 +  val extend = I;
    3.21 +  fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
    3.22      {intros=intros2, graph=graph2, eqns=eqns2}) =
    3.23      {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
    3.24       graph = Graph.merge (K true) (graph1, graph2),
    3.25       eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
    3.26    fun print _ _ = ();
    3.27 -end;
    3.28 +end);
    3.29  
    3.30 -structure CodegenData = TheoryDataFun(CodegenArgs);
    3.31  
    3.32  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    3.33    string_of_thm thm);
     4.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Jun 17 18:33:03 2005 +0200
     4.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Jun 17 18:33:05 2005 +0200
     4.3 @@ -16,18 +16,17 @@
     4.4  
     4.5  open Codegen;
     4.6  
     4.7 -structure CodegenArgs =
     4.8 -struct
     4.9 +structure CodegenData = TheoryDataFun
    4.10 +(struct
    4.11    val name = "HOL/recfun_codegen";
    4.12    type T = thm list Symtab.table;
    4.13    val empty = Symtab.empty;
    4.14    val copy = I;
    4.15 -  val prep_ext = I;
    4.16 -  val merge = Symtab.merge_multi' Drule.eq_thm_prop;
    4.17 +  val extend = I;
    4.18 +  fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
    4.19    fun print _ _ = ();
    4.20 -end;
    4.21 +end);
    4.22  
    4.23 -structure CodegenData = TheoryDataFun(CodegenArgs);
    4.24  
    4.25  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    4.26  val lhs_of = fst o dest_eqn o prop_of;
     5.1 --- a/src/HOL/Tools/refute.ML	Fri Jun 17 18:33:03 2005 +0200
     5.2 +++ b/src/HOL/Tools/refute.ML	Fri Jun 17 18:33:05 2005 +0200
     5.3 @@ -183,8 +183,8 @@
     5.4  			 parameters: string Symtab.table};
     5.5  		val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
     5.6  		val copy = I;
     5.7 -		val prep_ext = I;
     5.8 -		fun merge
     5.9 +		val extend = I;
    5.10 +		fun merge _
    5.11  			({interpreters = in1, printers = pr1, parameters = pa1},
    5.12  			 {interpreters = in2, printers = pr2, parameters = pa2}) =
    5.13  			{interpreters = rev (merge_alists (rev in1) (rev in2)),
     6.1 --- a/src/HOL/arith_data.ML	Fri Jun 17 18:33:03 2005 +0200
     6.2 +++ b/src/HOL/arith_data.ML	Fri Jun 17 18:33:05 2005 +0200
     6.3 @@ -201,24 +201,22 @@
     6.4  
     6.5  (* arith theory data *)
     6.6  
     6.7 -structure ArithTheoryDataArgs =
     6.8 -struct
     6.9 +structure ArithTheoryData = TheoryDataFun
    6.10 +(struct
    6.11    val name = "HOL/arith";
    6.12    type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string  list, presburger: (int -> tactic) option};
    6.13  
    6.14    val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
    6.15    val copy = I;
    6.16 -  val prep_ext = I;
    6.17 -  fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
    6.18 +  val extend = I;
    6.19 +  fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
    6.20               {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
    6.21     {splits = Drule.merge_rules (splits1, splits2),
    6.22      inj_consts = merge_lists inj_consts1 inj_consts2,
    6.23      discrete = merge_lists discrete1 discrete2,
    6.24      presburger = (case presburger1 of NONE => presburger2 | p => p)};
    6.25    fun print _ _ = ();
    6.26 -end;
    6.27 -
    6.28 -structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
    6.29 +end);
    6.30  
    6.31  fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
    6.32    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
    6.33 @@ -360,7 +358,7 @@
    6.34    | decomp2 data _ = NONE
    6.35  
    6.36  fun decomp sg =
    6.37 -  let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
    6.38 +  let val {discrete, inj_consts, ...} = ArithTheoryData.get sg
    6.39    in decomp2 (sg,discrete,inj_consts) end
    6.40  
    6.41  fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
    6.42 @@ -458,12 +456,12 @@
    6.43  
    6.44  fun raw_arith_tac ex i st =
    6.45    refute_tac (K true)
    6.46 -   (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    6.47 +   (REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.sign_of_thm st))))
    6.48     ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
    6.49     i st;
    6.50  
    6.51  fun presburger_tac i st =
    6.52 -  (case ArithTheoryData.get_sg (sign_of_thm st) of
    6.53 +  (case ArithTheoryData.get (sign_of_thm st) of
    6.54       {presburger = SOME tac, ...} =>
    6.55         (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
    6.56     | _ => no_tac st);
     7.1 --- a/src/Provers/classical.ML	Fri Jun 17 18:33:03 2005 +0200
     7.2 +++ b/src/Provers/classical.ML	Fri Jun 17 18:33:05 2005 +0200
     7.3 @@ -79,10 +79,10 @@
     7.4    val appSWrappers      : claset -> wrapper
     7.5    val appWrappers       : claset -> wrapper
     7.6  
     7.7 -  val claset_ref_of_sg: Sign.sg -> claset ref
     7.8    val claset_ref_of: theory -> claset ref
     7.9 -  val claset_of_sg: Sign.sg -> claset
    7.10 +  val claset_ref_of_sg: theory -> claset ref    (*obsolete*)
    7.11    val claset_of: theory -> claset
    7.12 +  val claset_of_sg: theory -> claset            (*obsolete*)
    7.13    val CLASET: (claset -> tactic) -> tactic
    7.14    val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    7.15    val claset: unit -> claset
    7.16 @@ -826,23 +826,22 @@
    7.17  
    7.18  (* theory data kind 'Provers/claset' *)
    7.19  
    7.20 -structure GlobalClasetArgs =
    7.21 -struct
    7.22 +structure GlobalClaset = TheoryDataFun
    7.23 +(struct
    7.24    val name = "Provers/claset";
    7.25    type T = claset ref * context_cs;
    7.26  
    7.27    val empty = (ref empty_cs, empty_context_cs);
    7.28 -  fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;            (*create new reference!*)
    7.29 -  val prep_ext = copy;
    7.30 -  fun merge ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
    7.31 +  fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
    7.32 +  val extend = copy;
    7.33 +  fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
    7.34      (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
    7.35    fun print _ (ref cs, _) = print_cs cs;
    7.36 -end;
    7.37 +end);
    7.38  
    7.39 -structure GlobalClaset = TheoryDataFun(GlobalClasetArgs);
    7.40  val print_claset = GlobalClaset.print;
    7.41 -val claset_ref_of_sg = #1 o GlobalClaset.get_sg;
    7.42  val claset_ref_of = #1 o GlobalClaset.get;
    7.43 +val claset_ref_of_sg = claset_ref_of;
    7.44  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    7.45  
    7.46  fun map_context_cs f = GlobalClaset.map (apsnd
    7.47 @@ -851,14 +850,14 @@
    7.48  
    7.49  (* access claset *)
    7.50  
    7.51 -val claset_of_sg = ! o claset_ref_of_sg;
    7.52 -val claset_of = claset_of_sg o Theory.sign_of;
    7.53 +val claset_of = ! o claset_ref_of;
    7.54 +val claset_of_sg = claset_of;
    7.55  
    7.56 -fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
    7.57 -fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
    7.58 +fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state;
    7.59 +fun CLASET' tacf i state = tacf (claset_of (Thm.theory_of_thm state)) i state;
    7.60  
    7.61  val claset = claset_of o Context.the_context;
    7.62 -val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
    7.63 +val claset_ref = claset_ref_of o Context.the_context;
    7.64  
    7.65  
    7.66  (* change claset *)
    7.67 @@ -885,15 +884,14 @@
    7.68  
    7.69  (* proof data kind 'Provers/claset' *)
    7.70  
    7.71 -structure LocalClasetArgs =
    7.72 -struct
    7.73 +structure LocalClaset = ProofDataFun
    7.74 +(struct
    7.75    val name = "Provers/claset";
    7.76    type T = claset;
    7.77    val init = claset_of;
    7.78    fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
    7.79 -end;
    7.80 +end);
    7.81  
    7.82 -structure LocalClaset = ProofDataFun(LocalClasetArgs);
    7.83  val print_local_claset = LocalClaset.print;
    7.84  val get_local_claset = LocalClaset.get;
    7.85  val put_local_claset = LocalClaset.put;
    7.86 @@ -921,7 +919,7 @@
    7.87    in (ctxt', #2 (DeltaClasetData.get ctxt'))
    7.88    end;
    7.89  
    7.90 -local 
    7.91 +local
    7.92  fun rename_thm' (ctxt,thm) =
    7.93    let val (new_ctxt, new_id) = delta_increment ctxt
    7.94        val new_name = "anon_cla_" ^ (string_of_int new_id)
    7.95 @@ -935,7 +933,7 @@
    7.96  fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
    7.97  
    7.98  end
    7.99 -     
   7.100 +
   7.101  
   7.102  (* attributes *)
   7.103  
   7.104 @@ -961,60 +959,60 @@
   7.105      let val thm_name = Thm.name_of_thm th
   7.106          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   7.107          val delta_cs = get_delta_claset ctxt'
   7.108 -	val new_dcs = delta_cs addSDs [th']
   7.109 -	val ctxt'' = put_delta_claset new_dcs ctxt'
   7.110 +        val new_dcs = delta_cs addSDs [th']
   7.111 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.112      in
   7.113 -	change_local_cs (op addSDs) (ctxt'',th)
   7.114 +        change_local_cs (op addSDs) (ctxt'',th)
   7.115      end;
   7.116  
   7.117 -fun safe_elim_local (ctxt, th)= 
   7.118 +fun safe_elim_local (ctxt, th)=
   7.119      let val thm_name = Thm.name_of_thm th
   7.120          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
   7.121          val delta_cs = get_delta_claset ctxt'
   7.122 -	val new_dcs = delta_cs addSEs [th']
   7.123 -	val ctxt'' = put_delta_claset new_dcs ctxt' 
   7.124 +        val new_dcs = delta_cs addSEs [th']
   7.125 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.126      in
   7.127 -	change_local_cs (op addSEs) (ctxt'',th)
   7.128 +        change_local_cs (op addSEs) (ctxt'',th)
   7.129      end;
   7.130  
   7.131 -fun safe_intro_local (ctxt, th) = 
   7.132 +fun safe_intro_local (ctxt, th) =
   7.133      let val thm_name = Thm.name_of_thm th
   7.134          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
   7.135          val delta_cs = get_delta_claset ctxt'
   7.136 -	val new_dcs = delta_cs addSIs [th']
   7.137 -	val ctxt'' = put_delta_claset new_dcs ctxt'
   7.138 +        val new_dcs = delta_cs addSIs [th']
   7.139 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.140      in
   7.141 -	change_local_cs (op addSIs) (ctxt'',th)
   7.142 +        change_local_cs (op addSIs) (ctxt'',th)
   7.143      end;
   7.144  
   7.145 -fun haz_dest_local (ctxt, th)= 
   7.146 +fun haz_dest_local (ctxt, th)=
   7.147      let val thm_name = Thm.name_of_thm th
   7.148          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th)
   7.149          val delta_cs = get_delta_claset ctxt'
   7.150 -	val new_dcs = delta_cs addDs [th']
   7.151 -	val ctxt'' = put_delta_claset new_dcs ctxt'
   7.152 +        val new_dcs = delta_cs addDs [th']
   7.153 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.154      in
   7.155 -	change_local_cs (op addDs) (ctxt'',th)
   7.156 +        change_local_cs (op addDs) (ctxt'',th)
   7.157      end;
   7.158  
   7.159  fun haz_elim_local (ctxt,th) =
   7.160      let val thm_name = Thm.name_of_thm th
   7.161          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   7.162          val delta_cs = get_delta_claset ctxt'
   7.163 -	val new_dcs = delta_cs addEs [th']
   7.164 -	val ctxt'' = put_delta_claset new_dcs ctxt'
   7.165 -    in 
   7.166 -	change_local_cs (op addEs) (ctxt'',th)
   7.167 +        val new_dcs = delta_cs addEs [th']
   7.168 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.169 +    in
   7.170 +        change_local_cs (op addEs) (ctxt'',th)
   7.171      end;
   7.172  
   7.173 -fun haz_intro_local (ctxt,th) = 
   7.174 +fun haz_intro_local (ctxt,th) =
   7.175      let val thm_name = Thm.name_of_thm th
   7.176          val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   7.177          val delta_cs = get_delta_claset ctxt'
   7.178 -	val new_dcs = delta_cs addIs [th']
   7.179 -	val ctxt'' = put_delta_claset new_dcs ctxt'
   7.180 -    in 
   7.181 -	change_local_cs (op addIs) (ctxt'',th)
   7.182 +        val new_dcs = delta_cs addIs [th']
   7.183 +        val ctxt'' = put_delta_claset new_dcs ctxt'
   7.184 +    in
   7.185 +        change_local_cs (op addIs) (ctxt'',th)
   7.186      end;
   7.187  
   7.188  
     8.1 --- a/src/Pure/Isar/calculation.ML	Fri Jun 17 18:33:03 2005 +0200
     8.2 +++ b/src/Pure/Isar/calculation.ML	Fri Jun 17 18:33:05 2005 +0200
     8.3 @@ -32,43 +32,41 @@
     8.4  
     8.5  (** global and local calculation data **)
     8.6  
     8.7 -(* theory data kind 'Isar/calculation' *)
     8.8 +(* global calculation *)
     8.9  
    8.10  fun print_rules prt x (trans, sym) =
    8.11    [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
    8.12      Pretty.big_list "symmetry rules:" (map (prt x) sym)]
    8.13    |> Pretty.chunks |> Pretty.writeln;
    8.14  
    8.15 -structure GlobalCalculationArgs =
    8.16 -struct
    8.17 +structure GlobalCalculation = TheoryDataFun
    8.18 +(struct
    8.19    val name = "Isar/calculation";
    8.20    type T = thm NetRules.T * thm list
    8.21  
    8.22    val empty = (NetRules.elim, []);
    8.23    val copy = I;
    8.24 -  val prep_ext = I;
    8.25 -  fun merge ((trans1, sym1), (trans2, sym2)) =
    8.26 +  val extend = I;
    8.27 +  fun merge _ ((trans1, sym1), (trans2, sym2)) =
    8.28      (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
    8.29    val print = print_rules Display.pretty_thm_sg;
    8.30 -end;
    8.31 +end);
    8.32  
    8.33 -structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    8.34  val _ = Context.add_setup [GlobalCalculation.init];
    8.35  val print_global_rules = GlobalCalculation.print;
    8.36  
    8.37  
    8.38 -(* proof data kind 'Isar/calculation' *)
    8.39 +(* local calculation *)
    8.40  
    8.41 -structure LocalCalculationArgs =
    8.42 -struct
    8.43 +structure LocalCalculation = ProofDataFun
    8.44 +(struct
    8.45    val name = "Isar/calculation";
    8.46    type T = (thm NetRules.T * thm list) * (thm list * int) option;
    8.47  
    8.48    fun init thy = (GlobalCalculation.get thy, NONE);
    8.49    fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    8.50 -end;
    8.51 +end);
    8.52  
    8.53 -structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    8.54  val _ = Context.add_setup [LocalCalculation.init];
    8.55  val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    8.56  val print_local_rules = LocalCalculation.print;
     9.1 --- a/src/Pure/Isar/context_rules.ML	Fri Jun 17 18:33:03 2005 +0200
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Jun 17 18:33:05 2005 +0200
     9.3 @@ -126,9 +126,9 @@
     9.4  
     9.5    val empty = make_rules ~1 [] empty_netpairs ([], []);
     9.6    val copy = I;
     9.7 -  val prep_ext = I;
     9.8 +  val extend = I;
     9.9  
    9.10 -  fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    9.11 +  fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    9.12        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
    9.13      let
    9.14        val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
    9.15 @@ -147,15 +147,14 @@
    9.16  val _ = Context.add_setup [GlobalRules.init];
    9.17  val print_global_rules = GlobalRules.print;
    9.18  
    9.19 -structure LocalRulesArgs =
    9.20 -struct
    9.21 +structure LocalRules = ProofDataFun
    9.22 +(struct
    9.23    val name = GlobalRulesArgs.name;
    9.24    type T = GlobalRulesArgs.T;
    9.25    val init = GlobalRules.get;
    9.26    val print = print_rules ProofContext.pretty_thm;
    9.27 -end;
    9.28 +end);
    9.29  
    9.30 -structure LocalRules = ProofDataFun(LocalRulesArgs);
    9.31  val _ = Context.add_setup [LocalRules.init];
    9.32  val print_local_rules = LocalRules.print;
    9.33  
    9.34 @@ -175,22 +174,25 @@
    9.35        if k = k' then untaglist rest
    9.36        else x :: untaglist rest;
    9.37  
    9.38 -fun orderlist brls = 
    9.39 -    untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    9.40 -fun orderlist_no_weight brls = 
    9.41 -    untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    9.42 +fun orderlist brls =
    9.43 +  untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    9.44 +
    9.45 +fun orderlist_no_weight brls =
    9.46 +  untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    9.47  
    9.48  fun may_unify weighted t net =
    9.49    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
    9.50  
    9.51  fun find_erules _ [] = K []
    9.52    | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact));
    9.53 +
    9.54  fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
    9.55  
    9.56  fun find_rules_netpair weighted facts goal (inet, enet) =
    9.57    find_erules weighted facts enet @ find_irules weighted goal inet;
    9.58  
    9.59 -fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
    9.60 +fun find_rules weighted facts goals =
    9.61 +  map (find_rules_netpair weighted facts goals) o netpairs;
    9.62  
    9.63  
    9.64  (* wrappers *)
    9.65 @@ -268,5 +270,4 @@
    9.66  val addXDs_local = modifier (dest_query_local NONE);
    9.67  val delrules_local = modifier rule_del_local;
    9.68  
    9.69 -
    9.70  end;
    10.1 --- a/src/Pure/Isar/induct_attrib.ML	Fri Jun 17 18:33:03 2005 +0200
    10.2 +++ b/src/Pure/Isar/induct_attrib.ML	Fri Jun 17 18:33:05 2005 +0200
    10.3 @@ -85,7 +85,7 @@
    10.4    NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    10.5      Drule.eq_thm_prop (th1, th2));
    10.6  
    10.7 -fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    10.8 +fun lookup_rule (rs: rules) name = assoc_string (NetRules.rules rs, name);
    10.9  
   10.10  fun print_rules prt kind x rs =
   10.11    let val thms = map snd (NetRules.rules rs)
   10.12 @@ -109,8 +109,8 @@
   10.13      ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
   10.14       (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
   10.15    val copy = I;
   10.16 -  val prep_ext = I;
   10.17 -  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
   10.18 +  val extend = I;
   10.19 +  fun merge _ (((casesT1, casesS1), (inductT1, inductS1)),
   10.20        ((casesT2, casesS2), (inductT2, inductS2))) =
   10.21      ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   10.22        (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
   10.23 @@ -132,16 +132,15 @@
   10.24  
   10.25  (* proof data kind 'Isar/induction' *)
   10.26  
   10.27 -structure LocalInductArgs =
   10.28 -struct
   10.29 +structure LocalInduct = ProofDataFun
   10.30 +(struct
   10.31    val name = "Isar/induction";
   10.32    type T = GlobalInductArgs.T;
   10.33  
   10.34    fun init thy = GlobalInduct.get thy;
   10.35    fun print x = print_all_rules ProofContext.pretty_thm x;
   10.36 -end;
   10.37 +end);
   10.38  
   10.39 -structure LocalInduct = ProofDataFun(LocalInductArgs);
   10.40  val _ = Context.add_setup [LocalInduct.init];
   10.41  val print_local_rules = LocalInduct.print;
   10.42  val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   10.43 @@ -229,5 +228,4 @@
   10.44    [(casesN, cases_attr, "declaration of cases rule for type or set"),
   10.45     (inductN, induct_attr, "declaration of induction rule for type or set")]];
   10.46  
   10.47 -
   10.48  end;
    11.1 --- a/src/Pure/Isar/term_style.ML	Fri Jun 17 18:33:03 2005 +0200
    11.2 +++ b/src/Pure/Isar/term_style.ML	Fri Jun 17 18:33:05 2005 +0200
    11.3 @@ -20,19 +20,18 @@
    11.4  fun err_dup_styles names =
    11.5    error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
    11.6  
    11.7 -structure StyleArgs =
    11.8 -struct
    11.9 +structure StyleData = TheoryDataFun
   11.10 +(struct
   11.11    val name = "Isar/style";
   11.12    type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
   11.13    val empty = Symtab.empty;
   11.14    val copy = I;
   11.15 -  val prep_ext = I;
   11.16 -  fun merge tabs = Symtab.merge eq_snd tabs
   11.17 +  val extend = I;
   11.18 +  fun merge _ tabs = Symtab.merge eq_snd tabs
   11.19      handle Symtab.DUPS dups => err_dup_styles dups;
   11.20    fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
   11.21 -end;
   11.22 +end);
   11.23  
   11.24 -structure StyleData = TheoryDataFun(StyleArgs);
   11.25  val _ = Context.add_setup [StyleData.init];
   11.26  val print_styles = StyleData.print;
   11.27  
   11.28 @@ -52,16 +51,19 @@
   11.29  (* predefined styles *)
   11.30  
   11.31  fun style_binargs ctxt t =
   11.32 -  let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
   11.33 +  let
   11.34 +    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
   11.35 +      (Logic.strip_imp_concl t)
   11.36 +  in
   11.37      case concl of (_ $ l $ r) => (l, r)
   11.38      | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
   11.39    end;
   11.40  
   11.41  fun style_parm_premise i ctxt t =
   11.42 -  let val prems = Logic.strip_imp_prems t
   11.43 -  in if i <= length prems then List.nth(prems, i-1)
   11.44 -     else error ("Not enough premises for prem" ^ string_of_int i ^
   11.45 -                 " in propositon: " ^ ProofContext.string_of_term ctxt t)
   11.46 +  let val prems = Logic.strip_imp_prems t in
   11.47 +    if i <= length prems then List.nth (prems, i - 1)
   11.48 +    else error ("Not enough premises for prem" ^ string_of_int i ^
   11.49 +      " in propositon: " ^ ProofContext.string_of_term ctxt t)
   11.50    end;
   11.51  
   11.52  val _ = Context.add_setup
    12.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jun 17 18:33:03 2005 +0200
    12.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Jun 17 18:33:05 2005 +0200
    12.3 @@ -18,19 +18,18 @@
    12.4  
    12.5  (* theory data *)
    12.6  
    12.7 -structure IndCasesArgs =
    12.8 -struct
    12.9 +structure IndCasesData = TheoryDataFun
   12.10 +(struct
   12.11    val name = "ZF/ind_cases";
   12.12    type T = (simpset -> cterm -> thm) Symtab.table;
   12.13  
   12.14    val empty = Symtab.empty;
   12.15    val copy = I;
   12.16 -  val prep_ext = I;
   12.17 -  fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
   12.18 +  val extend = I;
   12.19 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   12.20    fun print _ _ = ();
   12.21 -end;
   12.22 +end);
   12.23  
   12.24 -structure IndCasesData = TheoryDataFun(IndCasesArgs);
   12.25  
   12.26  fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab));
   12.27