Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
--- a/doc-src/Logics/logics.bbl Fri Feb 16 17:24:51 1996 +0100
+++ b/doc-src/Logics/logics.bbl Fri Feb 16 18:00:47 1996 +0100
@@ -173,8 +173,9 @@
\bibitem{paulson-CADE}
Lawrence~C. Paulson.
\newblock A fixedpoint approach to implementing (co)inductive definitions.
-\newblock In Alan Bundy, editor, {\em 12th International Conference on
- Automated Deduction}, LNAI 814, pages 148--161. Springer, 1994.
+\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI
+ 814, pages 148--161. Springer, 1994.
+\newblock 12th international conference.
\bibitem{paulson-set-II}
Lawrence~C. Paulson.
--- a/src/FOLP/simp.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/FOLP/simp.ML Fri Feb 16 18:00:47 1996 +0100
@@ -135,7 +135,7 @@
in mk trans_thms end;
(*Applies tactic and returns the first resulting state, FAILS if none!*)
-fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
+fun one_result(tac,thm) = case Sequence.pull(tac thm) of
Some(thm',_) => thm'
| None => raise THM("Simplifier: could not continue", 0, [thm]);
@@ -211,7 +211,7 @@
resolve_tac congs 1 ORELSE refl1_tac
| Free _ => resolve_tac congs 1 ORELSE refl1_tac
| _ => refl1_tac))
- val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
+ val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
in thm'' end;
fun add_norm_tags congs =
@@ -336,19 +336,19 @@
in find_if(tm,0) end;
fun IF1_TAC cong_tac i =
- let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply(
- COND (if_rewritable ifc i) (DETERM(rtac ifth i))
- (Tactic(seq_try(ifths,ifcs))), thm)
- | seq_try([],_) thm = tapply(no_tac,thm)
- and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
- ORELSE Tactic one_subt, thm)
+ let fun seq_try (ifth::ifths,ifc::ifcs) thm =
+ (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
+ (seq_try(ifths,ifcs))) thm
+ | seq_try([],_) thm = no_tac thm
+ and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
and one_subt thm =
let val test = has_fewer_prems (nprems_of thm + 1)
- fun loop thm = tapply(COND test no_tac
- ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
- ORELSE (refl_tac i THEN Tactic loop)), thm)
- in tapply(cong_tac THEN Tactic loop, thm) end
- in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end;
+ fun loop thm =
+ COND test no_tac
+ ((try_rew THEN DEPTH_FIRST test (refl_tac i))
+ ORELSE (refl_tac i THEN loop)) thm
+ in (cong_tac THEN loop) thm end
+ in COND (may_match(case_consts,i)) try_rew no_tac end;
fun CASE_TAC (SS{cong_net,...}) i =
let val cong_tac = net_tac cong_net i
@@ -422,7 +422,7 @@
fun simp_lhs(thm,ss,anet,ats,cs) =
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
- else case Sequence.pull(tapply(cong_tac i,thm)) of
+ else case Sequence.pull(cong_tac i thm) of
Some(thm',_) =>
let val ps = prems_of thm and ps' = prems_of thm';
val n = length(ps')-length(ps);
@@ -455,12 +455,12 @@
thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
end
| None => if more
- then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
+ then rew((lhs_net_tac anet i THEN assume_tac i) thm,
thm,ss,anet,ats,cs,false)
else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
- case Sequence.pull(tapply(auto_tac i,thm)) of
+ case Sequence.pull(auto_tac i thm) of
Some(thm',_) => (ss,thm',anet,ats,cs)
| None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
in if !tracing
@@ -471,7 +471,7 @@
end;
fun if_exp(thm,ss,anet,ats,cs) =
- case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
+ case Sequence.pull (IF1_TAC (cong_tac i) i thm) of
Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
| None => (ss,thm,anet,ats,cs);
@@ -479,7 +479,7 @@
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
- | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
+ | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
| PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
@@ -496,10 +496,11 @@
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
let val cong_tac = net_tac cong_net
-in fn i => Tactic(fn thm =>
- if i <= 0 orelse nprems_of thm < i then Sequence.null
- else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
- THEN TRY(auto_tac i)
+in fn i =>
+ (fn thm =>
+ if i <= 0 orelse nprems_of thm < i then Sequence.null
+ else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
+ THEN TRY(auto_tac i)
end;
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
--- a/src/HOL/ex/meson.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/HOL/ex/meson.ML Fri Feb 16 18:00:47 1996 +0100
@@ -158,12 +158,10 @@
val prop_of = #prop o rep_thm;
(*Permits forward proof from rules that discharge assumptions*)
-fun forward_res nf state =
- case Sequence.pull
- (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)),
- state))
+fun forward_res nf st =
+ case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
of Some(th,_) => th
- | None => raise THM("forward_res", 0, [state]);
+ | None => raise THM("forward_res", 0, [st]);
(*Negation Normal Form*)
@@ -188,10 +186,10 @@
fun skolemize th =
if not (has_consts ["Ex"] (prop_of th)) then th
else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
- disj_exD, disj_exD1, disj_exD2]))
+ disj_exD, disj_exD1, disj_exD2]))
handle THM _ =>
skolemize (forward_res skolemize
- (tryres (th, [conj_forward, disj_forward, all_forward])))
+ (tryres (th, [conj_forward, disj_forward, all_forward])))
handle THM _ => forward_res skolemize (th RS ex_forward);
@@ -243,8 +241,7 @@
(METAHYPS (resop (cnf_nil seen)) 1) THEN
(STATE (fn st' =>
METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
- in Sequence.list_of_s (tapply(tac, th RS disj_forward)) @ ths
- end
+ in Sequence.list_of_s (tac (th RS disj_forward)) @ ths end
and cnf_nil seen th = cnf_aux seen (th,[]);
(*Top-level call to cnf -- it's safe to reset name_ref*)
@@ -266,13 +263,13 @@
qed "disj_forward2";
(*Forward proof, passing extra assumptions as theorems to the tactic*)
-fun forward_res2 nf hyps state =
+fun forward_res2 nf hyps st =
case Sequence.pull
- (tapply(REPEAT
- (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1),
- state))
+ (REPEAT
+ (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+ st)
of Some(th,_) => th
- | None => raise THM("forward_res2", 0, [state]);
+ | None => raise THM("forward_res2", 0, [st]);
(*Remove duplicates in P|Q by assuming ~P in Q
rls (initially []) accumulates assumptions of the form P==>False*)
--- a/src/HOLCF/ax_ops/thy_ops.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/HOLCF/ax_ops/thy_ops.ML Fri Feb 16 18:00:47 1996 +0100
@@ -8,21 +8,21 @@
For a short english description of the new sections
write to regensbu@informatik.tu-muenchen.de.
-TODO: vielleicht AST-Darstellung mit "op name" statt _I_...
+TODO: maybe AST-representation with "op name" instead of _I_...
*)
signature THY_OPS =
sig
- (* continuous mixfixes (extension of datatype PrivateSyntax.Mixfix.mixfix) *)
+ (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
datatype cmixfix =
- Mixfix of PrivateSyntax.Mixfix.mixfix |
+ Mixfix of Mixfix.mixfix |
CInfixl of int |
CInfixr of int |
CMixfix of string * int list *int;
exception CINFIX of cmixfix;
- val cmixfix_to_mixfix : cmixfix -> PrivateSyntax.Mixfix.mixfix;
+ val cmixfix_to_mixfix : cmixfix -> Mixfix.mixfix;
(* theory extenders : *)
val add_ops : {curried: bool, total: bool, strict: bool} ->
@@ -54,7 +54,7 @@
(* the extended copy of mixfix *)
datatype cmixfix =
- Mixfix of PrivateSyntax.Mixfix.mixfix |
+ Mixfix of Mixfix.mixfix |
CInfixl of int |
CInfixr of int |
CMixfix of string * int list *int;
@@ -125,36 +125,36 @@
fun oldstyle ((name,typ,Mixfix(x))::tl) =
(name,typ,x)::(oldstyle tl)
| oldstyle ((name,typ,CInfixl(i))::tl) =
- (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn)::
+ (mk_internal_name name,typ,Mixfix.NoSyn)::
(oldstyle tl)
| oldstyle ((name,typ,CInfixr(i))::tl) =
- (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn)::
+ (mk_internal_name name,typ,Mixfix.NoSyn)::
(oldstyle tl)
| oldstyle ((name,typ,CMixfix(x))::tl) =
- (name,typ,PrivateSyntax.Mixfix.NoSyn)::
+ (name,typ,Mixfix.NoSyn)::
(oldstyle tl)
| oldstyle [] = [];
(* generating the external purely syntactical infix functions.
Called by add_ext_axioms(_i) *)
fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
- (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixl(i))::
+ (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
(syn_decls curried sign tl)
| syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
- (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixr(i))::
+ (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
(syn_decls curried sign tl)
| syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
(*####
- ("@"^name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x))::
+ ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
####**)
- (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x))::
+ (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
(syn_decls curried sign tl)
| syn_decls curried sign (_::tl) = syn_decls curried sign tl
| syn_decls _ _ [] = [];
(* generating the translation rules. Called by add_ext_axioms(_i) *)
-local open PrivateSyntax.Ast in
+local open Ast in
fun xrules_of true ((name,typ,CInfixl(i))::tail) =
((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
(mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
--- a/src/HOLCF/domain/theorems.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/HOLCF/domain/theorems.ML Fri Feb 16 18:00:47 1996 +0100
@@ -46,10 +46,10 @@
fun REPEAT_DETERM_UNTIL p tac =
let fun drep st = if p st then Sequence.single st
- else (case Sequence.pull(tapply(tac,st)) of
+ else (case Sequence.pull(tac st) of
None => Sequence.null
| Some(st',_) => drep st')
-in Tactic drep end;
+in drep end;
val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in
--- a/src/Provers/astar.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Provers/astar.ML Fri Feb 16 18:00:47 1996 +0100
@@ -21,7 +21,7 @@
infix THEN_ASTAR;
val trace_ASTAR = ref false;
-fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) =
+fun tf0 THEN_ASTAR (satp, costf, tac) =
let val tf = tracify trace_ASTAR tac;
fun bfs (news,nprfs,level) =
let fun cost thm = (level,costf level thm,thm)
--- a/src/Provers/ind.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Provers/ind.ML Fri Feb 16 18:00:47 1996 +0100
@@ -40,22 +40,23 @@
fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
(*Generalizes over all free variables, with the named var outermost.*)
-fun all_frees_tac (var:string) i = Tactic(fn thm =>
+fun all_frees_tac (var:string) i thm =
let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
val frees' = sort(op>)(frees \ var) @ [var]
- in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
+ in foldl (qnt_tac i) (all_tac,frees') thm end;
fun REPEAT_SIMP_TAC simp_tac n i =
-let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
- let val k = length(prems_of thm)
- in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
- end, thm)
-in Tactic repeat end;
+let fun repeat thm =
+ (COND (has_fewer_prems n) all_tac
+ let val k = nprems_of thm
+ in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
+ thm
+in repeat end;
-fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
- resolve_tac [sch] i THEN
- REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
+fun ALL_IND_TAC sch simp_tac i thm =
+ (resolve_tac [sch] i THEN
+ REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
fun IND_TAC sch simp_tac var =
all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
--- a/src/Provers/simp.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Provers/simp.ML Fri Feb 16 18:00:47 1996 +0100
@@ -129,7 +129,7 @@
in mk trans_thms end;
(*Applies tactic and returns the first resulting state, FAILS if none!*)
-fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
+fun one_result(tac,thm) = case Sequence.pull(tac thm) of
Some(thm',_) => thm'
| None => raise THM("Simplifier: could not continue", 0, [thm]);
@@ -205,7 +205,7 @@
resolve_tac congs 1 ORELSE refl1_tac
| Free _ => resolve_tac congs 1 ORELSE refl1_tac
| _ => refl1_tac))
- val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
+ val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
in thm'' end;
fun add_norm_tags congs =
@@ -357,18 +357,18 @@
fun split_tac (cong_tac,splits,split_consts) i =
let fun seq_try (split::splits,a::bs) thm = tapply(
COND (splittable a i) (DETERM(resolve_tac[split]i))
- (Tactic(seq_try(splits,bs))), thm)
- | seq_try([],_) thm = tapply(no_tac,thm)
- and try_rew thm = tapply(Tactic(seq_try(splits,split_consts))
- ORELSE Tactic one_subt, thm)
+ ((seq_try(splits,bs))), thm)
+ | seq_try([],_) thm = no_tac thm
+ and try_rew thm = tapply((seq_try(splits,split_consts))
+ ORELSE one_subt, thm)
and one_subt thm =
let val test = has_fewer_prems (nprems_of thm + 1)
fun loop thm = tapply(COND test no_tac
- ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
- ORELSE (refl_tac i THEN Tactic loop)), thm)
- in tapply(cong_tac THEN Tactic loop, thm) end
+ ((try_rew THEN DEPTH_FIRST test (refl_tac i))
+ ORELSE (refl_tac i THEN loop)), thm)
+ in (cong_tac THEN loop) thm end
in if null splits then no_tac
- else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac
+ else COND (may_match(split_consts,i)) try_rew no_tac
end;
fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i =
@@ -443,7 +443,7 @@
fun simp_lhs(thm,ss,anet,ats,cs) =
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
- else case Sequence.pull(tapply(cong_tac i,thm)) of
+ else case Sequence.pull(cong_tac i thm) of
Some(thm',_) =>
let val ps = prems_of thm and ps' = prems_of thm';
val n = length(ps')-length(ps);
@@ -481,7 +481,7 @@
else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
- case Sequence.pull(tapply(auto_tac i,thm)) of
+ case Sequence.pull(auto_tac i thm) of
Some(thm',_) => (ss,thm',anet,ats,cs)
| None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
in if !tracing
@@ -501,7 +501,7 @@
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
- | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
+ | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
| PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss
--- a/src/Provers/simplifier.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Provers/simplifier.ML Fri Feb 16 18:00:47 1996 +0100
@@ -36,7 +36,7 @@
val Asm_full_simp_tac: int -> tactic
end;
-functor SimplifierFun():SIMPLIFIER =
+structure Simplifier :SIMPLIFIER =
struct
datatype simpset =
@@ -158,14 +158,11 @@
(fn n => if n<0 then all_tac else no_tac)
in DEPTH_SOLVE(solve1_tac) end
- fun simp_loop i thm =
- tapply(asm_rewrite_goal_tac mode solve_all_tac mss i THEN
- (finish_tac (prems_of_mss mss) i ORELSE looper i),
- thm)
+ fun simp_loop_tac i thm =
+ (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
+ (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
- and simp_loop_tac i = Tactic(simp_loop i)
-
in simp_loop_tac end;
val asm_full_simp_tac = gen_simp_tac (true,true);
--- a/src/Pure/Thy/ROOT.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/ROOT.ML Fri Feb 16 18:00:47 1996 +0100
@@ -8,17 +8,10 @@
use "thy_scan.ML";
use "thy_parse.ML";
-
-structure ThyScan = ThyScanFun(Scanner);
-structure ThyParse = ThyParseFun(structure Symtab = Symtab
- and ThyScan = ThyScan);
-
use "thy_syn.ML";
use "thm_database.ML";
use "../../Provers/simplifier.ML";
-structure Simplifier = SimplifierFun();
-
use "thy_read.ML";
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
@@ -26,10 +19,6 @@
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
open ThmDB ReadThy;
-(* hide functors; saves space in PolyML *)
-functor ThyScanFun() = struct end;
-functor ThyParseFun() = struct end;
-functor SimplifierFun() = struct end;
fun init_thy_reader () =
use_string
--- a/src/Pure/Thy/thm_database.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thm_database.ML Fri Feb 16 18:00:47 1996 +0100
@@ -15,7 +15,7 @@
indexed by the constants they contain*)
signature THMDB =
-sig
+ sig
val thm_db: thm_db_type ref
val store_thm_db: string * thm -> thm
val delete_thm_db: theory -> unit
@@ -23,7 +23,7 @@
val findI: int -> (string * thm)list
val findEs: int -> (string * thm)list
val findE: int -> int -> (string * thm)list
-end;
+ end;
functor ThmDBFun(): THMDB =
struct
--- a/src/Pure/Thy/thy_parse.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML Fri Feb 16 18:00:47 1996 +0100
@@ -10,7 +10,7 @@
infix 0 ||;
signature THY_PARSE =
-sig
+ sig
type token
val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c
val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
@@ -66,9 +66,10 @@
val mk_pair: string * string -> string
val mk_triple: string * string * string -> string
val strip_quotes: string -> string
-end;
+ end;
-functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
+
+structure ThyParse : THY_PARSE=
struct
open ThyScan;
@@ -517,5 +518,4 @@
axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
section "instance" "" instance_decl];
-
end;
--- a/src/Pure/Thy/thy_scan.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thy_scan.ML Fri Feb 16 18:00:47 1996 +0100
@@ -6,17 +6,17 @@
*)
signature THY_SCAN =
-sig
+ sig
datatype token_kind =
Keyword | Ident | LongIdent | TypeVar | Nat | String | Verbatim | EOF
val name_of_kind: token_kind -> string
type lexicon
val make_lexicon: string list -> lexicon
val tokenize: lexicon -> string -> (token_kind * string * int) list
-end;
+ end;
-functor ThyScanFun(Scanner: SCANNER): THY_SCAN =
+structure ThyScan : THY_SCAN =
struct
open Scanner;
--- a/src/Pure/Thy/thy_syn.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Pure/Thy/thy_syn.ML Fri Feb 16 18:00:47 1996 +0100
@@ -6,26 +6,25 @@
*)
signature THY_SYN_DATA =
-sig
+ sig
val user_keywords: string list
val user_sections: (string * (ThyParse.token list -> (string * string)
* ThyParse.token list)) list
-end;
+ end;
signature THY_SYN =
-sig
+ sig
val parse: string -> string -> string
-end;
+ end;
-functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
+functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
struct
-open ThyParse ThySynData;
+val syntax =
+ ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
+ (ThyParse.pure_sections @ Data.user_sections);
-val syntax =
- make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
-
-val parse = parse_thy syntax;
+val parse = ThyParse.parse_thy syntax;
end;
--- a/src/Tools/agrep Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Tools/agrep Fri Feb 16 18:00:47 1996 +0100
@@ -1,2 +1,2 @@
#! /bin/csh
-grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML
+grep "$*" */*.ML */*/*.ML
--- a/src/ZF/ROOT.ML Fri Feb 16 17:24:51 1996 +0100
+++ b/src/ZF/ROOT.ML Fri Feb 16 18:00:47 1996 +0100
@@ -12,9 +12,8 @@
writeln banner;
(*For Pure/tactic?? A crude way of adding structure to rules*)
-fun CHECK_SOLVED (Tactic tf) =
- Tactic (fn state =>
- case Sequence.pull (tf state) of
+fun CHECK_SOLVED tac st =
+ case Sequence.pull (tac st) of
None => error"DO_GOAL: tactic list failed"
| Some(x,_) =>
if has_fewer_prems 1 x then
@@ -22,7 +21,7 @@
else (writeln"DO_GOAL: unsolved goals!!";
writeln"Final proof state was ...";
print_goals (!goals_limit) x;
- raise ERROR));
+ raise ERROR);
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));