# HG changeset patch
# User paulson
# Date 824470458 -3600
# Node ID bb7f99a0a6f0464069d3a559900bd9da0c3e6497
# Parent  b2de3b3277b8ff9fc9e5db6278d1cba3a0199eec
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

diff -r b2de3b3277b8 -r bb7f99a0a6f0 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/pattern.ML	Fri Feb 16 12:34:18 1996 +0100
@@ -13,7 +13,7 @@
 *)
 
 signature PATTERN =
-sig
+  sig
   type type_sig
   type sg
   type env
@@ -25,13 +25,11 @@
   exception Unif
   exception MATCH
   exception Pattern
-end;
+  end;
 
-functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN =
+structure Pattern : PATTERN =
 struct
 
-structure Type = Sign.Type;
-
 type type_sig = Type.type_sig
 type sg = Sign.sg
 type env = Envir.env
diff -r b2de3b3277b8 -r bb7f99a0a6f0 src/Pure/sequence.ML
--- a/src/Pure/sequence.ML	Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/sequence.ML	Fri Feb 16 12:34:18 1996 +0100
@@ -35,7 +35,7 @@
   end;
 
 
-functor SequenceFun () : SEQUENCE = 
+structure Sequence : SEQUENCE = 
 struct
     
 datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
diff -r b2de3b3277b8 -r bb7f99a0a6f0 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/sign.ML	Fri Feb 16 12:34:18 1996 +0100
@@ -6,84 +6,71 @@
 *)
 
 signature SIGN =
-sig
-  structure Symtab: SYMTAB
-  structure Syntax: SYNTAX
-  structure Type: TYPE
-  sharing Symtab = Type.Symtab
-  local open Type Syntax in
-    type sg
-    val rep_sg: sg ->
-      {tsig: type_sig,
-       const_tab: typ Symtab.table,
-       syn: syntax,
-       stamps: string ref list}
-    val subsig: sg * sg -> bool
-    val eq_sg: sg * sg -> bool
-    val same_sg: sg * sg -> bool
-    val is_draft: sg -> bool
-    val const_type: sg -> string -> typ option
-    val classes: sg -> class list
-    val subsort: sg -> sort * sort -> bool
-    val nodup_Vars: term -> unit
-    val norm_sort: sg -> sort -> sort
-    val nonempty_sort: sg -> sort list -> sort -> bool
-    val print_sg: sg -> unit
-    val pretty_sg: sg -> Pretty.T
-    val pprint_sg: sg -> pprint_args -> unit
-    val pretty_term: sg -> term -> Pretty.T
-    val pretty_typ: sg -> typ -> Pretty.T
-    val pretty_sort: sort -> Pretty.T
-    val string_of_term: sg -> term -> string
-    val string_of_typ: sg -> typ -> string
-    val pprint_term: sg -> term -> pprint_args -> unit
-    val pprint_typ: sg -> typ -> pprint_args -> unit
-    val certify_typ: sg -> typ -> typ
-    val certify_term: sg -> term -> term * typ * int
-    val read_typ: sg * (indexname -> sort option) -> string -> typ
-    val exn_type_msg: sg -> string * typ list * term list -> string
-    val infer_types: sg -> (indexname -> typ option) ->
-      (indexname -> sort option) -> string list -> bool
-      -> term list * typ -> int * term * (indexname * typ) list
-    val add_classes: (class * class list) list -> sg -> sg
-    val add_classrel: (class * class) list -> sg -> sg
-    val add_defsort: sort -> sg -> sg
-    val add_types: (string * int * mixfix) list -> sg -> sg
-    val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
-    val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
-    val add_arities: (string * sort list * sort) list -> sg -> sg
-    val add_consts: (string * string * mixfix) list -> sg -> sg
-    val add_consts_i: (string * typ * mixfix) list -> sg -> sg
-    val add_syntax: (string * string * mixfix) list -> sg -> sg
-    val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
-    val add_trfuns:
-      (string * (ast list -> ast)) list *
-      (string * (term list -> term)) list *
-      (string * (term list -> term)) list *
-      (string * (ast list -> ast)) list -> sg -> sg
-    val add_trrules: (string * string) trrule list -> sg -> sg
-    val add_trrules_i: ast trrule list -> sg -> sg
-    val add_name: string -> sg -> sg
-    val make_draft: sg -> sg
-    val merge: sg * sg -> sg
-    val proto_pure: sg
-    val pure: sg
-    val cpure: sg
-    val const_of_class: class -> string
-    val class_of_const: string -> class
-  end
-end;
+  sig
+  type sg
+  val rep_sg: sg -> {tsig: Type.type_sig,
+		     const_tab: typ Symtab.table,
+		     syn: Syntax.syntax,
+		     stamps: string ref list}
+  val subsig: sg * sg -> bool
+  val eq_sg: sg * sg -> bool
+  val same_sg: sg * sg -> bool
+  val is_draft: sg -> bool
+  val const_type: sg -> string -> typ option
+  val classes: sg -> class list
+  val subsort: sg -> sort * sort -> bool
+  val nodup_Vars: term -> unit
+  val norm_sort: sg -> sort -> sort
+  val nonempty_sort: sg -> sort list -> sort -> bool
+  val print_sg: sg -> unit
+  val pretty_sg: sg -> Pretty.T
+  val pprint_sg: sg -> pprint_args -> unit
+  val pretty_term: sg -> term -> Pretty.T
+  val pretty_typ: sg -> typ -> Pretty.T
+  val pretty_sort: sort -> Pretty.T
+  val string_of_term: sg -> term -> string
+  val string_of_typ: sg -> typ -> string
+  val pprint_term: sg -> term -> pprint_args -> unit
+  val pprint_typ: sg -> typ -> pprint_args -> unit
+  val certify_typ: sg -> typ -> typ
+  val certify_term: sg -> term -> term * typ * int
+  val read_typ: sg * (indexname -> sort option) -> string -> typ
+  val exn_type_msg: sg -> string * typ list * term list -> string
+  val infer_types: sg -> (indexname -> typ option) ->
+    (indexname -> sort option) -> string list -> bool
+    -> term list * typ -> int * term * (indexname * typ) list
+  val add_classes: (class * class list) list -> sg -> sg
+  val add_classrel: (class * class) list -> sg -> sg
+  val add_defsort: sort -> sg -> sg
+  val add_types: (string * int * mixfix) list -> sg -> sg
+  val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
+  val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
+  val add_arities: (string * sort list * sort) list -> sg -> sg
+  val add_consts: (string * string * mixfix) list -> sg -> sg
+  val add_consts_i: (string * typ * mixfix) list -> sg -> sg
+  val add_syntax: (string * string * mixfix) list -> sg -> sg
+  val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
+  val add_trfuns:
+    (string * (ast list -> ast)) list *
+    (string * (term list -> term)) list *
+    (string * (term list -> term)) list *
+    (string * (ast list -> ast)) list -> sg -> sg
+  val add_trrules: (string * string) trrule list -> sg -> sg
+  val add_trrules_i: ast trrule list -> sg -> sg
+  val add_name: string -> sg -> sg
+  val make_draft: sg -> sg
+  val merge: sg * sg -> sg
+  val proto_pure: sg
+  val pure: sg
+  val cpure: sg
+  val const_of_class: class -> string
+  val class_of_const: string -> class
+  end;
 
-functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
+structure Sign : SIGN =
 struct
 
-structure Symtab = Type.Symtab;
-structure Syntax = Syntax;
-structure BasicSyntax: BASIC_SYNTAX = Syntax;
-structure Pretty = Syntax.Pretty;
-structure Type = Type;
-open BasicSyntax Type;
-
+local open Type Syntax in
 
 (** datatype sg **)
 
@@ -92,7 +79,7 @@
 
 datatype sg =
   Sg of {
-    tsig: type_sig,                 (*order-sorted signature of types*)
+    tsig: Type.type_sig,                 (*order-sorted signature of types*)
     const_tab: typ Symtab.table,    (*types of constants*)
     syn: Syntax.syntax,             (*syntax for parsing and printing*)
     stamps: string ref list};       (*unique theory indentifier*)
@@ -605,4 +592,5 @@
   |> add_syntax Syntax.pure_applC_syntax
   |> add_name "CPure";
 
+end
 end;
diff -r b2de3b3277b8 -r bb7f99a0a6f0 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/tactic.ML	Fri Feb 16 12:34:18 1996 +0100
@@ -7,24 +7,21 @@
 *)
 
 signature TACTIC =
-sig
-  structure Tactical: TACTICAL and Net: NET
-  local open Tactical Tactical.Thm Net
-  in
+  sig
   val ares_tac: thm list -> int -> tactic
   val asm_rewrite_goal_tac:
         bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
   val assume_tac: int -> tactic
   val atac: int ->tactic
   val bimatch_from_nets_tac: 
-      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
+      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
   val bimatch_tac: (bool*thm)list -> int -> tactic
   val biresolve_from_nets_tac: 
-      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
+      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
   val biresolve_tac: (bool*thm)list -> int -> tactic
-  val build_net: thm list -> (int*thm) net
-  val build_netpair:    (int*(bool*thm)) net * (int*(bool*thm)) net ->
-      (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
+  val build_net: thm list -> (int*thm) Net.net
+  val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
+      (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
   val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
   val compose_tac: (bool * thm * int) -> int -> tactic 
   val cut_facts_tac: thm list -> int -> tactic
@@ -47,13 +44,13 @@
   val forw_inst_tac: (string*string)list -> thm -> int -> tactic
   val freeze: thm -> thm   
   val insert_tagged_brl:  ('a*(bool*thm)) * 
-                    (('a*(bool*thm))net * ('a*(bool*thm))net) ->
-                    ('a*(bool*thm))net * ('a*(bool*thm))net
+                    (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
+                    ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
   val is_fact: thm -> bool
   val lessb: (bool * thm) * (bool * thm) -> bool
   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
   val make_elim: thm -> thm
-  val match_from_net_tac: (int*thm) net -> int -> tactic
+  val match_from_net_tac: (int*thm) Net.net -> int -> tactic
   val match_tac: thm list -> int -> tactic
   val metacut_tac: thm -> int -> tactic   
   val net_bimatch_tac: (bool*thm) list -> int -> tactic
@@ -65,7 +62,7 @@
   val prune_params_tac: tactic
   val rename_tac: string -> int -> tactic
   val rename_last_tac: string -> string list -> int -> tactic
-  val resolve_from_net_tac: (int*thm) net -> int -> tactic
+  val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic
   val resolve_tac: thm list -> int -> tactic
   val res_inst_tac: (string*string)list -> thm -> int -> tactic   
   val rewrite_goals_tac: thm list -> tactic
@@ -78,28 +75,18 @@
   val subgoals_tac: string list -> int -> tactic
   val subgoals_of_brl: bool * thm -> int
   val trace_goalno_tac: (int -> tactic) -> int -> tactic
-  end
-end;
+  end;
 
 
-functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
-		   Tactical: TACTICAL and Net: NET
-	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
+structure Tactic : TACTIC = 
 struct
-structure Tactical = Tactical;
-structure Thm = Tactical.Thm;
-structure Net = Net;
-structure Sequence = Thm.Sequence;
-structure Sign = Thm.Sign;
-local open Tactical Tactical.Thm Drule
-in
 
-(*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
-fun trace_goalno_tac tf i = Tactic (fn state => 
-    case Sequence.pull(tapply(tf i, state)) of
+(*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
+fun trace_goalno_tac tac i st =  
+    case Sequence.pull(tac i st) of
 	None    => Sequence.null
       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
-    			 Sequence.seqof(fn()=> seqcell)));
+    			 Sequence.seqof(fn()=> seqcell));
 
 fun string_of (a,0) = a
   | string_of (a,i) = a ^ "_" ^ string_of_int i;
@@ -115,16 +102,15 @@
   in  instantiate ([],insts) fth  end;
 
 (*Makes a rule by applying a tactic to an existing rule*)
-fun rule_by_tactic (Tactic tf) rl =
-    case Sequence.pull(tf (freeze (standard rl))) of
+fun rule_by_tactic tac rl =
+    case Sequence.pull(tac (freeze (standard rl))) of
 	None        => raise THM("rule_by_tactic", 0, [rl])
       | Some(rl',_) => standard rl';
  
 (*** Basic tactics ***)
 
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
-fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
-			                 handle THM _ => Sequence.null);
+fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
 
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
 fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
@@ -182,9 +168,9 @@
 val flexflex_tac = PRIMSEQ flexflex_rule;
 
 (*Lift and instantiate a rule wrt the given state and subgoal number *)
-fun lift_inst_rule (state, i, sinsts, rule) =
-let val {maxidx,sign,...} = rep_thm state
-    val (_, _, Bi, _) = dest_state(state,i)
+fun lift_inst_rule (st, i, sinsts, rule) =
+let val {maxidx,sign,...} = rep_thm st
+    val (_, _, Bi, _) = dest_state(st,i)
     val params = Logic.strip_params Bi	        (*params of subgoal i*)
     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
     val paramTs = map #2 params
@@ -198,14 +184,14 @@
     fun lifttvar((a,i),ctyp) =
 	let val {T,sign} = rep_ctyp ctyp
 	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
-    val rts = types_sorts rule and (types,sorts) = types_sorts state
+    val rts = types_sorts rule and (types,sorts) = types_sorts st
     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
       | types'(ixn) = types ixn;
     val used = add_term_tvarnames
-                  (#prop(rep_thm state) $ #prop(rep_thm rule),[])
+                  (#prop(rep_thm st) $ #prop(rep_thm rule),[])
     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
 in instantiate (map lifttvar Tinsts, map liftpair insts)
-               (lift_rule (state,i) rule)
+               (lift_rule (st,i) rule)
 end;
 
 
@@ -214,8 +200,8 @@
 
 (*compose version: arguments are as for bicompose.*)
 fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
-  STATE ( fn state => 
-	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
+  STATE ( fn st => 
+	   compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
 			nsubgoal) i
 	   handle TERM (msg,_) => (writeln msg;  no_tac)
 		| THM  (msg,_,_) => (writeln msg;  no_tac) );
@@ -232,7 +218,7 @@
 fun res_inst_tac sinsts rule i =
     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
 
-(*eresolve (elimination) version*)
+(*eresolve elimination version*)
 fun eres_inst_tac sinsts rule i =
     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
 
@@ -400,7 +386,7 @@
 (*** Meta-Rewriting Tactics ***)
 
 fun result1 tacf mss thm =
-  case Sequence.pull(tapply(tacf mss,thm)) of
+  case Sequence.pull(tacf mss thm) of
     None => None
   | Some(thm,_) => Some(thm);
 
@@ -417,7 +403,7 @@
 fun rewtac def = rewrite_goals_tac [def];
 
 
-(*** Tactic for folding definitions, handling critical pairs ***)
+(*** for folding definitions, handling critical pairs ***)
 
 (*The depth of nesting in a term*)
 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
@@ -458,8 +444,8 @@
     | c::_ => error ("Illegal character: " ^ c)
   end;
 
-(*Rename recent parameters using names generated from (a) and the suffixes,
-  provided the string (a), which represents a term, is an identifier. *)
+(*Rename recent parameters using names generated from a and the suffixes,
+  provided the string a, which represents a term, is an identifier. *)
 fun rename_last_tac a sufs i = 
   let val names = map (curry op^ a) sufs
   in  if Syntax.is_identifier a
@@ -470,9 +456,8 @@
 (*Prunes all redundant parameters from the proof state by rewriting*)
 val prune_params_tac = rewrite_tac [triv_forall_equality];
 
-(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
- * right to left if n is positive, and from left to right if n is negative.
- *)
+(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
+  right to left if n is positive, and from left to right if n is negative.*)
 fun rotate_tac n =
   let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
   in if n >= 0 then rot n
@@ -480,4 +465,5 @@
   end;
 
 end;
-end;
+
+open Tactic;