Elimination of fully-functorial style.
authorpaulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512ce37c64244c0
parent 1511 09354d37a5ab
child 1513 c318e1bbecca
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
doc-src/Logics/logics.bbl
src/FOLP/simp.ML
src/HOL/ex/meson.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/domain/theorems.ML
src/Provers/astar.ML
src/Provers/ind.ML
src/Provers/simp.ML
src/Provers/simplifier.ML
src/Pure/Thy/ROOT.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_parse.ML
src/Pure/Thy/thy_scan.ML
src/Pure/Thy/thy_syn.ML
src/Tools/agrep
src/ZF/ROOT.ML
     1.1 --- a/doc-src/Logics/logics.bbl	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/doc-src/Logics/logics.bbl	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -173,8 +173,9 @@
     1.4  \bibitem{paulson-CADE}
     1.5  Lawrence~C. Paulson.
     1.6  \newblock A fixedpoint approach to implementing (co)inductive definitions.
     1.7 -\newblock In Alan Bundy, editor, {\em 12th International Conference on
     1.8 -  Automated Deduction}, LNAI 814, pages 148--161. Springer, 1994.
     1.9 +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI
    1.10 +  814, pages 148--161. Springer, 1994.
    1.11 +\newblock 12th international conference.
    1.12  
    1.13  \bibitem{paulson-set-II}
    1.14  Lawrence~C. Paulson.
     2.1 --- a/src/FOLP/simp.ML	Fri Feb 16 17:24:51 1996 +0100
     2.2 +++ b/src/FOLP/simp.ML	Fri Feb 16 18:00:47 1996 +0100
     2.3 @@ -135,7 +135,7 @@
     2.4  in mk trans_thms end;
     2.5  
     2.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     2.7 -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
     2.8 +fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     2.9          Some(thm',_) => thm'
    2.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    2.11  
    2.12 @@ -211,7 +211,7 @@
    2.13                               resolve_tac congs 1 ORELSE refl1_tac
    2.14                  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    2.15                  | _ => refl1_tac))
    2.16 -    val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
    2.17 +    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    2.18  in thm'' end;
    2.19  
    2.20  fun add_norm_tags congs =
    2.21 @@ -336,19 +336,19 @@
    2.22      in find_if(tm,0) end;
    2.23  
    2.24  fun IF1_TAC cong_tac i =
    2.25 -    let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply(
    2.26 -                COND (if_rewritable ifc i) (DETERM(rtac ifth i))
    2.27 -                        (Tactic(seq_try(ifths,ifcs))), thm)
    2.28 -              | seq_try([],_) thm = tapply(no_tac,thm)
    2.29 -        and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
    2.30 -                                 ORELSE Tactic one_subt, thm)
    2.31 +    let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
    2.32 +                (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
    2.33 +                        (seq_try(ifths,ifcs))) thm
    2.34 +              | seq_try([],_) thm = no_tac thm
    2.35 +        and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
    2.36          and one_subt thm =
    2.37                  let val test = has_fewer_prems (nprems_of thm + 1)
    2.38 -                    fun loop thm = tapply(COND test no_tac
    2.39 -                        ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
    2.40 -                         ORELSE (refl_tac i THEN Tactic loop)), thm)
    2.41 -                in tapply(cong_tac THEN Tactic loop, thm) end
    2.42 -    in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end;
    2.43 +                    fun loop thm = 
    2.44 +			COND test no_tac
    2.45 +                          ((try_rew THEN DEPTH_FIRST test (refl_tac i))
    2.46 +			   ORELSE (refl_tac i THEN loop)) thm
    2.47 +                in (cong_tac THEN loop) thm end
    2.48 +    in COND (may_match(case_consts,i)) try_rew no_tac end;
    2.49  
    2.50  fun CASE_TAC (SS{cong_net,...}) i =
    2.51  let val cong_tac = net_tac cong_net i
    2.52 @@ -422,7 +422,7 @@
    2.53  fun simp_lhs(thm,ss,anet,ats,cs) =
    2.54      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    2.55      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    2.56 -    else case Sequence.pull(tapply(cong_tac i,thm)) of
    2.57 +    else case Sequence.pull(cong_tac i thm) of
    2.58              Some(thm',_) =>
    2.59                      let val ps = prems_of thm and ps' = prems_of thm';
    2.60                          val n = length(ps')-length(ps);
    2.61 @@ -455,12 +455,12 @@
    2.62                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    2.63              end
    2.64      | None => if more
    2.65 -            then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
    2.66 +            then rew((lhs_net_tac anet i THEN assume_tac i) thm,
    2.67                       thm,ss,anet,ats,cs,false)
    2.68              else (ss,thm,anet,ats,cs);
    2.69  
    2.70  fun try_true(thm,ss,anet,ats,cs) =
    2.71 -    case Sequence.pull(tapply(auto_tac i,thm)) of
    2.72 +    case Sequence.pull(auto_tac i thm) of
    2.73        Some(thm',_) => (ss,thm',anet,ats,cs)
    2.74      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    2.75                in if !tracing
    2.76 @@ -471,7 +471,7 @@
    2.77                end;
    2.78  
    2.79  fun if_exp(thm,ss,anet,ats,cs) =
    2.80 -        case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
    2.81 +        case Sequence.pull (IF1_TAC (cong_tac i) i thm) of
    2.82                  Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
    2.83                | None => (ss,thm,anet,ats,cs);
    2.84  
    2.85 @@ -479,7 +479,7 @@
    2.86            MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
    2.87          | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
    2.88          | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
    2.89 -        | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
    2.90 +        | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
    2.91          | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
    2.92          | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
    2.93          | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
    2.94 @@ -496,10 +496,11 @@
    2.95  
    2.96  fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
    2.97  let val cong_tac = net_tac cong_net
    2.98 -in fn i => Tactic(fn thm =>
    2.99 -        if i <= 0 orelse nprems_of thm < i then Sequence.null
   2.100 -        else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   2.101 -           THEN TRY(auto_tac i)
   2.102 +in fn i => 
   2.103 +    (fn thm =>
   2.104 +     if i <= 0 orelse nprems_of thm < i then Sequence.null
   2.105 +     else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   2.106 +    THEN TRY(auto_tac i)
   2.107  end;
   2.108  
   2.109  val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
     3.1 --- a/src/HOL/ex/meson.ML	Fri Feb 16 17:24:51 1996 +0100
     3.2 +++ b/src/HOL/ex/meson.ML	Fri Feb 16 18:00:47 1996 +0100
     3.3 @@ -158,12 +158,10 @@
     3.4  val prop_of = #prop o rep_thm;
     3.5  
     3.6  (*Permits forward proof from rules that discharge assumptions*)
     3.7 -fun forward_res nf state =
     3.8 -  case Sequence.pull
     3.9 -        (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), 
    3.10 -                state))
    3.11 +fun forward_res nf st =
    3.12 +  case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
    3.13    of Some(th,_) => th
    3.14 -   | None => raise THM("forward_res", 0, [state]);
    3.15 +   | None => raise THM("forward_res", 0, [st]);
    3.16  
    3.17  
    3.18  (*Negation Normal Form*)
    3.19 @@ -188,10 +186,10 @@
    3.20  fun skolemize th = 
    3.21    if not (has_consts ["Ex"] (prop_of th)) then th
    3.22    else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    3.23 -                          disj_exD, disj_exD1, disj_exD2]))
    3.24 +			      disj_exD, disj_exD1, disj_exD2]))
    3.25      handle THM _ => 
    3.26          skolemize (forward_res skolemize
    3.27 -                (tryres (th, [conj_forward, disj_forward, all_forward])))
    3.28 +		   (tryres (th, [conj_forward, disj_forward, all_forward])))
    3.29      handle THM _ => forward_res skolemize (th RS ex_forward);
    3.30  
    3.31  
    3.32 @@ -243,8 +241,7 @@
    3.33          (METAHYPS (resop (cnf_nil seen)) 1) THEN
    3.34          (STATE (fn st' => 
    3.35                  METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
    3.36 -    in  Sequence.list_of_s (tapply(tac, th RS disj_forward))  @  ths
    3.37 -    end
    3.38 +    in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
    3.39  and cnf_nil seen th = cnf_aux seen (th,[]);
    3.40  
    3.41  (*Top-level call to cnf -- it's safe to reset name_ref*)
    3.42 @@ -266,13 +263,13 @@
    3.43  qed "disj_forward2";
    3.44  
    3.45  (*Forward proof, passing extra assumptions as theorems to the tactic*)
    3.46 -fun forward_res2 nf hyps state =
    3.47 +fun forward_res2 nf hyps st =
    3.48    case Sequence.pull
    3.49 -        (tapply(REPEAT 
    3.50 -           (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), 
    3.51 -           state))
    3.52 +        (REPEAT 
    3.53 +	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
    3.54 +	 st)
    3.55    of Some(th,_) => th
    3.56 -   | None => raise THM("forward_res2", 0, [state]);
    3.57 +   | None => raise THM("forward_res2", 0, [st]);
    3.58  
    3.59  (*Remove duplicates in P|Q by assuming ~P in Q
    3.60    rls (initially []) accumulates assumptions of the form P==>False*)
     4.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Fri Feb 16 17:24:51 1996 +0100
     4.2 +++ b/src/HOLCF/ax_ops/thy_ops.ML	Fri Feb 16 18:00:47 1996 +0100
     4.3 @@ -8,21 +8,21 @@
     4.4  For a short english description of the new sections
     4.5  write to regensbu@informatik.tu-muenchen.de. 
     4.6  
     4.7 -TODO: vielleicht AST-Darstellung mit "op name" statt _I_...
     4.8 +TODO: maybe AST-representation with "op name" instead of _I_...
     4.9  
    4.10  *)
    4.11  
    4.12  signature THY_OPS =
    4.13  sig
    4.14 - (* continuous mixfixes (extension of datatype PrivateSyntax.Mixfix.mixfix) *)
    4.15 + (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
    4.16   datatype cmixfix =
    4.17 -    Mixfix of PrivateSyntax.Mixfix.mixfix |
    4.18 +    Mixfix of Mixfix.mixfix |
    4.19      CInfixl of int | 
    4.20      CInfixr of int |
    4.21      CMixfix of string * int list *int;
    4.22  
    4.23   exception CINFIX of cmixfix;
    4.24 - val cmixfix_to_mixfix : cmixfix ->  PrivateSyntax.Mixfix.mixfix;
    4.25 + val cmixfix_to_mixfix : cmixfix ->  Mixfix.mixfix;
    4.26  
    4.27   (* theory extenders : *)
    4.28   val add_ops          : {curried: bool, total: bool, strict: bool} ->
    4.29 @@ -54,7 +54,7 @@
    4.30  
    4.31  (* the extended copy of mixfix *)
    4.32  datatype cmixfix =
    4.33 -    Mixfix of PrivateSyntax.Mixfix.mixfix |
    4.34 +    Mixfix of Mixfix.mixfix |
    4.35      CInfixl of int |
    4.36      CInfixr of int |
    4.37      CMixfix of string * int list *int;
    4.38 @@ -125,36 +125,36 @@
    4.39  fun oldstyle ((name,typ,Mixfix(x))::tl) = 
    4.40           (name,typ,x)::(oldstyle tl)
    4.41    | oldstyle ((name,typ,CInfixl(i))::tl) = 
    4.42 -         (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn)::
    4.43 +         (mk_internal_name name,typ,Mixfix.NoSyn)::
    4.44           (oldstyle tl)
    4.45    | oldstyle ((name,typ,CInfixr(i))::tl) =
    4.46 -         (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn)::
    4.47 +         (mk_internal_name name,typ,Mixfix.NoSyn)::
    4.48           (oldstyle tl) 
    4.49    | oldstyle ((name,typ,CMixfix(x))::tl) =
    4.50 -         (name,typ,PrivateSyntax.Mixfix.NoSyn)::
    4.51 +         (name,typ,Mixfix.NoSyn)::
    4.52           (oldstyle tl) 
    4.53    | oldstyle [] = [];
    4.54  
    4.55  (* generating the external purely syntactical infix functions. 
    4.56     Called by add_ext_axioms(_i) *)
    4.57  fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
    4.58 -     (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixl(i))::
    4.59 +     (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
    4.60        (syn_decls curried sign tl)
    4.61    | syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
    4.62 -     (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixr(i))::
    4.63 +     (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
    4.64        (syn_decls curried sign tl)
    4.65    | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
    4.66  (*####
    4.67 -     ("@"^name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x))::
    4.68 +     ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
    4.69  ####**)
    4.70 -     (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x))::
    4.71 +     (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
    4.72  
    4.73        (syn_decls curried sign tl)
    4.74    | syn_decls curried sign (_::tl) = syn_decls curried sign tl
    4.75    | syn_decls _ _ [] = [];
    4.76  
    4.77  (* generating the translation rules. Called by add_ext_axioms(_i) *)
    4.78 -local open PrivateSyntax.Ast in 
    4.79 +local open Ast in 
    4.80  fun xrules_of true ((name,typ,CInfixl(i))::tail) = 
    4.81      ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
    4.82       (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
     5.1 --- a/src/HOLCF/domain/theorems.ML	Fri Feb 16 17:24:51 1996 +0100
     5.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Feb 16 18:00:47 1996 +0100
     5.3 @@ -46,10 +46,10 @@
     5.4  
     5.5  fun REPEAT_DETERM_UNTIL p tac = 
     5.6  let fun drep st = if p st then Sequence.single st
     5.7 -                          else (case Sequence.pull(tapply(tac,st)) of
     5.8 +                          else (case Sequence.pull(tac st) of
     5.9                                    None        => Sequence.null
    5.10                                  | Some(st',_) => drep st')
    5.11 -in Tactic drep end;
    5.12 +in drep end;
    5.13  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
    5.14  
    5.15  local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in
     6.1 --- a/src/Provers/astar.ML	Fri Feb 16 17:24:51 1996 +0100
     6.2 +++ b/src/Provers/astar.ML	Fri Feb 16 18:00:47 1996 +0100
     6.3 @@ -21,7 +21,7 @@
     6.4  infix THEN_ASTAR;
     6.5  val trace_ASTAR = ref false; 
     6.6  
     6.7 -fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) = 
     6.8 +fun tf0 THEN_ASTAR (satp, costf, tac) = 
     6.9    let val tf = tracify trace_ASTAR tac;   
    6.10        fun bfs (news,nprfs,level) =
    6.11        let fun cost thm = (level,costf level thm,thm)
     7.1 --- a/src/Provers/ind.ML	Fri Feb 16 17:24:51 1996 +0100
     7.2 +++ b/src/Provers/ind.ML	Fri Feb 16 18:00:47 1996 +0100
     7.3 @@ -40,22 +40,23 @@
     7.4  fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
     7.5  
     7.6  (*Generalizes over all free variables, with the named var outermost.*)
     7.7 -fun all_frees_tac (var:string) i = Tactic(fn thm =>
     7.8 +fun all_frees_tac (var:string) i thm = 
     7.9      let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
    7.10          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
    7.11          val frees' = sort(op>)(frees \ var) @ [var]
    7.12 -    in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
    7.13 +    in foldl (qnt_tac i) (all_tac,frees') thm end;
    7.14  
    7.15  fun REPEAT_SIMP_TAC simp_tac n i =
    7.16 -let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
    7.17 -	let val k = length(prems_of thm)
    7.18 -	in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
    7.19 -	end, thm)
    7.20 -in Tactic repeat end;
    7.21 +let fun repeat thm = 
    7.22 +        (COND (has_fewer_prems n) all_tac
    7.23 +	 let val k = nprems_of thm
    7.24 +	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
    7.25 +	thm
    7.26 +in repeat end;
    7.27  
    7.28 -fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
    7.29 -	resolve_tac [sch] i THEN
    7.30 -	REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
    7.31 +fun ALL_IND_TAC sch simp_tac i thm = 
    7.32 +	(resolve_tac [sch] i THEN
    7.33 +	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
    7.34  
    7.35  fun IND_TAC sch simp_tac var =
    7.36  	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
     8.1 --- a/src/Provers/simp.ML	Fri Feb 16 17:24:51 1996 +0100
     8.2 +++ b/src/Provers/simp.ML	Fri Feb 16 18:00:47 1996 +0100
     8.3 @@ -129,7 +129,7 @@
     8.4  in mk trans_thms end;
     8.5  
     8.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     8.7 -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
     8.8 +fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     8.9  	Some(thm',_) => thm'
    8.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    8.11  
    8.12 @@ -205,7 +205,7 @@
    8.13  			     resolve_tac congs 1 ORELSE refl1_tac
    8.14  		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
    8.15  		| _ => refl1_tac))
    8.16 -    val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
    8.17 +    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    8.18  in thm'' end;
    8.19  
    8.20  fun add_norm_tags congs =
    8.21 @@ -357,18 +357,18 @@
    8.22  fun split_tac (cong_tac,splits,split_consts) i =
    8.23      let fun seq_try (split::splits,a::bs) thm = tapply(
    8.24  		COND (splittable a i) (DETERM(resolve_tac[split]i))
    8.25 -			(Tactic(seq_try(splits,bs))), thm)
    8.26 -	      | seq_try([],_) thm = tapply(no_tac,thm)
    8.27 -	and try_rew thm = tapply(Tactic(seq_try(splits,split_consts))
    8.28 -				 ORELSE Tactic one_subt, thm)
    8.29 +			((seq_try(splits,bs))), thm)
    8.30 +	      | seq_try([],_) thm = no_tac thm
    8.31 +	and try_rew thm = tapply((seq_try(splits,split_consts))
    8.32 +				 ORELSE one_subt, thm)
    8.33  	and one_subt thm =
    8.34  		let val test = has_fewer_prems (nprems_of thm + 1)
    8.35  		    fun loop thm = tapply(COND test no_tac
    8.36 -			((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
    8.37 -			 ORELSE (refl_tac i THEN Tactic loop)), thm)
    8.38 -		in tapply(cong_tac THEN Tactic loop, thm) end
    8.39 +			((try_rew THEN DEPTH_FIRST test (refl_tac i))
    8.40 +			 ORELSE (refl_tac i THEN loop)), thm)
    8.41 +		in (cong_tac THEN loop) thm end
    8.42      in if null splits then no_tac
    8.43 -       else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac
    8.44 +       else COND (may_match(split_consts,i)) try_rew no_tac
    8.45      end;
    8.46  
    8.47  fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i =
    8.48 @@ -443,7 +443,7 @@
    8.49  fun simp_lhs(thm,ss,anet,ats,cs) =
    8.50      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    8.51      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    8.52 -    else case Sequence.pull(tapply(cong_tac i,thm)) of
    8.53 +    else case Sequence.pull(cong_tac i thm) of
    8.54  	    Some(thm',_) =>
    8.55  		    let val ps = prems_of thm and ps' = prems_of thm';
    8.56  			val n = length(ps')-length(ps);
    8.57 @@ -481,7 +481,7 @@
    8.58  	    else (ss,thm,anet,ats,cs);
    8.59  
    8.60  fun try_true(thm,ss,anet,ats,cs) =
    8.61 -    case Sequence.pull(tapply(auto_tac i,thm)) of
    8.62 +    case Sequence.pull(auto_tac i thm) of
    8.63        Some(thm',_) => (ss,thm',anet,ats,cs)
    8.64      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    8.65  	      in if !tracing
    8.66 @@ -501,7 +501,7 @@
    8.67  	  MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
    8.68  	| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
    8.69  	| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
    8.70 -	| REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
    8.71 +	| REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
    8.72  	| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
    8.73  	| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
    8.74  	| PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss
     9.1 --- a/src/Provers/simplifier.ML	Fri Feb 16 17:24:51 1996 +0100
     9.2 +++ b/src/Provers/simplifier.ML	Fri Feb 16 18:00:47 1996 +0100
     9.3 @@ -36,7 +36,7 @@
     9.4    val Asm_full_simp_tac: int -> tactic
     9.5  end;
     9.6  
     9.7 -functor SimplifierFun():SIMPLIFIER =
     9.8 +structure Simplifier :SIMPLIFIER =
     9.9  struct
    9.10  
    9.11  datatype simpset =
    9.12 @@ -158,14 +158,11 @@
    9.13                            (fn n => if n<0 then all_tac else no_tac)
    9.14          in DEPTH_SOLVE(solve1_tac) end
    9.15  
    9.16 -      fun simp_loop i thm =
    9.17 -        tapply(asm_rewrite_goal_tac mode solve_all_tac mss i THEN
    9.18 -               (finish_tac (prems_of_mss mss) i  ORELSE  looper i),
    9.19 -               thm)
    9.20 +      fun simp_loop_tac i thm =
    9.21 +	  (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
    9.22 +	   (finish_tac (prems_of_mss mss) i  ORELSE  looper i))  thm
    9.23        and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
    9.24        and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
    9.25 -      and simp_loop_tac i = Tactic(simp_loop i)
    9.26 -
    9.27    in simp_loop_tac end;
    9.28  
    9.29  val asm_full_simp_tac = gen_simp_tac (true,true);
    10.1 --- a/src/Pure/Thy/ROOT.ML	Fri Feb 16 17:24:51 1996 +0100
    10.2 +++ b/src/Pure/Thy/ROOT.ML	Fri Feb 16 18:00:47 1996 +0100
    10.3 @@ -8,17 +8,10 @@
    10.4  
    10.5  use "thy_scan.ML";
    10.6  use "thy_parse.ML";
    10.7 -
    10.8 -structure ThyScan = ThyScanFun(Scanner);
    10.9 -structure ThyParse = ThyParseFun(structure Symtab = Symtab
   10.10 -  and ThyScan = ThyScan);
   10.11 -
   10.12  use "thy_syn.ML";
   10.13  use "thm_database.ML";
   10.14  use "../../Provers/simplifier.ML";
   10.15  
   10.16 -structure Simplifier = SimplifierFun();
   10.17 -
   10.18  use "thy_read.ML";
   10.19  
   10.20  structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
   10.21 @@ -26,10 +19,6 @@
   10.22  structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
   10.23  open ThmDB ReadThy;
   10.24  
   10.25 -(* hide functors; saves space in PolyML *)
   10.26 -functor ThyScanFun() = struct end;
   10.27 -functor ThyParseFun() = struct end;
   10.28 -functor SimplifierFun() = struct end;
   10.29  
   10.30  fun init_thy_reader () =
   10.31    use_string
    11.1 --- a/src/Pure/Thy/thm_database.ML	Fri Feb 16 17:24:51 1996 +0100
    11.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Feb 16 18:00:47 1996 +0100
    11.3 @@ -15,7 +15,7 @@
    11.4                   indexed by the constants they contain*)
    11.5  
    11.6  signature THMDB =
    11.7 -sig
    11.8 +  sig
    11.9    val thm_db: thm_db_type ref
   11.10    val store_thm_db: string * thm -> thm
   11.11    val delete_thm_db: theory -> unit
   11.12 @@ -23,7 +23,7 @@
   11.13    val findI:         int -> (string * thm)list
   11.14    val findEs:        int -> (string * thm)list
   11.15    val findE:  int -> int -> (string * thm)list
   11.16 -end;
   11.17 +  end;
   11.18  
   11.19  functor ThmDBFun(): THMDB =
   11.20  struct
    12.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Feb 16 17:24:51 1996 +0100
    12.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Feb 16 18:00:47 1996 +0100
    12.3 @@ -10,7 +10,7 @@
    12.4  infix 0 ||;
    12.5  
    12.6  signature THY_PARSE =
    12.7 -sig
    12.8 +  sig
    12.9    type token
   12.10    val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c
   12.11    val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   12.12 @@ -66,9 +66,10 @@
   12.13    val mk_pair: string * string -> string
   12.14    val mk_triple: string * string * string -> string
   12.15    val strip_quotes: string -> string
   12.16 -end;
   12.17 +  end;
   12.18  
   12.19 -functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
   12.20 +
   12.21 +structure ThyParse : THY_PARSE=
   12.22  struct
   12.23  
   12.24  open ThyScan;
   12.25 @@ -517,5 +518,4 @@
   12.26    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   12.27    section "instance" "" instance_decl];
   12.28  
   12.29 -
   12.30  end;
    13.1 --- a/src/Pure/Thy/thy_scan.ML	Fri Feb 16 17:24:51 1996 +0100
    13.2 +++ b/src/Pure/Thy/thy_scan.ML	Fri Feb 16 18:00:47 1996 +0100
    13.3 @@ -6,17 +6,17 @@
    13.4  *)
    13.5  
    13.6  signature THY_SCAN =
    13.7 -sig
    13.8 +  sig
    13.9    datatype token_kind =
   13.10      Keyword | Ident | LongIdent | TypeVar | Nat | String | Verbatim | EOF
   13.11    val name_of_kind: token_kind -> string
   13.12    type lexicon
   13.13    val make_lexicon: string list -> lexicon
   13.14    val tokenize: lexicon -> string -> (token_kind * string * int) list
   13.15 -end;
   13.16 +  end;
   13.17  
   13.18  
   13.19 -functor ThyScanFun(Scanner: SCANNER): THY_SCAN =
   13.20 +structure ThyScan : THY_SCAN =
   13.21  struct
   13.22  
   13.23  open Scanner;
    14.1 --- a/src/Pure/Thy/thy_syn.ML	Fri Feb 16 17:24:51 1996 +0100
    14.2 +++ b/src/Pure/Thy/thy_syn.ML	Fri Feb 16 18:00:47 1996 +0100
    14.3 @@ -6,26 +6,25 @@
    14.4  *)
    14.5  
    14.6  signature THY_SYN_DATA =
    14.7 -sig
    14.8 +  sig
    14.9    val user_keywords: string list
   14.10    val user_sections: (string * (ThyParse.token list -> (string * string)
   14.11      * ThyParse.token list)) list
   14.12 -end;
   14.13 +  end;
   14.14  
   14.15  signature THY_SYN =
   14.16 -sig
   14.17 +  sig
   14.18    val parse: string -> string -> string
   14.19 -end;
   14.20 +  end;
   14.21  
   14.22 -functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
   14.23 +functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
   14.24  struct
   14.25  
   14.26 -open ThyParse ThySynData;
   14.27 +val syntax =
   14.28 +  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
   14.29 +		       (ThyParse.pure_sections @ Data.user_sections);
   14.30  
   14.31 -val syntax =
   14.32 -  make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
   14.33 -
   14.34 -val parse = parse_thy syntax;
   14.35 +val parse = ThyParse.parse_thy syntax;
   14.36  
   14.37  end;
   14.38  
    15.1 --- a/src/Tools/agrep	Fri Feb 16 17:24:51 1996 +0100
    15.2 +++ b/src/Tools/agrep	Fri Feb 16 18:00:47 1996 +0100
    15.3 @@ -1,2 +1,2 @@
    15.4  #! /bin/csh
    15.5 -grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML 
    15.6 +grep "$*" */*.ML */*/*.ML 
    16.1 --- a/src/ZF/ROOT.ML	Fri Feb 16 17:24:51 1996 +0100
    16.2 +++ b/src/ZF/ROOT.ML	Fri Feb 16 18:00:47 1996 +0100
    16.3 @@ -12,9 +12,8 @@
    16.4  writeln banner;
    16.5  
    16.6  (*For Pure/tactic??  A crude way of adding structure to rules*)
    16.7 -fun CHECK_SOLVED (Tactic tf) = 
    16.8 -  Tactic (fn state => 
    16.9 -    case Sequence.pull (tf state) of
   16.10 +fun CHECK_SOLVED tac st =
   16.11 +    case Sequence.pull (tac st) of
   16.12          None => error"DO_GOAL: tactic list failed"
   16.13        | Some(x,_) => 
   16.14                  if has_fewer_prems 1 x then
   16.15 @@ -22,7 +21,7 @@
   16.16                  else (writeln"DO_GOAL: unsolved goals!!";
   16.17                        writeln"Final proof state was ...";
   16.18                        print_goals (!goals_limit) x;
   16.19 -                      raise ERROR));
   16.20 +                      raise ERROR);
   16.21  
   16.22  fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
   16.23