Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

--- a/src/Pure/ROOT.ML	Thu Feb 15 10:51:22 1996 +0100
+++ b/src/Pure/ROOT.ML	Fri Feb 16 11:35:52 1996 +0100
@@ -40,47 +40,9 @@
 use "goals.ML";
 use "axclass.ML";
 
-(*Will be visible to all object-logics.*)
-structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
-structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
-structure Sequence = SequenceFun();
-structure Envir = EnvirFun();
-structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
-structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
-                           and Sequence=Sequence and Pattern=Pattern);
-structure Net = NetFun();
-structure Logic = LogicFun(structure Unify=Unify and Net=Net);
-structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
-                             and Pattern=Pattern);
-structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
-structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
-structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
-                             and Tactical=Tactical and Net=Net);
-structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
-                           and Tactic=Tactic and Pattern=Pattern);
-structure AxClass = AxClassFun(structure Logic = Logic
-  and Goals = Goals and Tactic = Tactic);
-open BasicSyntax Thm Drule Tactical Tactic Goals;
-
 structure Pure = struct val thy = pure_thy end;
 structure CPure = struct val thy = cpure_thy end;
 
-(* hide functors; saves space in PolyML *)
-functor TypeFun() = struct end;
-functor SignFun() = struct end;
-functor SequenceFun() = struct end;
-functor EnvirFun() = struct end;
-functor PatternFun() = struct end;
-functor UnifyFun() = struct end;
-functor NetFun() = struct end;
-functor LogicFun() = struct end;
-functor ThmFun() = struct end;
-functor DruleFun() = struct end;
-functor TacticalFun() = struct end;
-functor TacticFun() = struct end;
-functor GoalsFun() = struct end;
-functor AxClassFun() = struct end;
-
 (*Theory parser and loader*)
 cd "Thy";
 use "ROOT.ML";

--- a/src/Pure/axclass.ML	Thu Feb 15 10:51:22 1996 +0100
+++ b/src/Pure/axclass.ML	Fri Feb 16 11:35:52 1996 +0100
@@ -6,43 +6,30 @@
 *)
 
 signature AX_CLASS =
-sig
-  structure Tactical: TACTICAL
-  local open Tactical Tactical.Thm in
-    val add_thms_as_axms: (string * thm) list -> theory -> theory
-    val add_classrel_thms: thm list -> theory -> theory
-    val add_arity_thms: thm list -> theory -> theory
-    val add_axclass: class * class list -> (string * string) list
-      -> theory -> theory
-    val add_axclass_i: class * class list -> (string * term) list
-      -> theory -> theory
-    val add_inst_subclass: class * class -> string list -> thm list
-      -> tactic option -> theory -> theory
-    val add_inst_arity: string * sort list * class list -> string list
-      -> thm list -> tactic option -> theory -> theory
-    val axclass_tac: theory -> thm list -> tactic
-    val prove_subclass: theory -> class * class -> thm list
-      -> tactic option -> thm
-    val prove_arity: theory -> string * sort list * class -> thm list
-      -> tactic option -> thm
-    val goal_subclass: theory -> class * class -> thm list
-    val goal_arity: theory -> string * sort list * class -> thm list
-  end
-end;
+  sig
+  val add_thms_as_axms: (string * thm) list -> theory -> theory
+  val add_classrel_thms: thm list -> theory -> theory
+  val add_arity_thms: thm list -> theory -> theory
+  val add_axclass: class * class list -> (string * string) list
+    -> theory -> theory
+  val add_axclass_i: class * class list -> (string * term) list
+    -> theory -> theory
+  val add_inst_subclass: class * class -> string list -> thm list
+    -> tactic option -> theory -> theory
+  val add_inst_arity: string * sort list * class list -> string list
+    -> thm list -> tactic option -> theory -> theory
+  val axclass_tac: theory -> thm list -> tactic
+  val prove_subclass: theory -> class * class -> thm list
+    -> tactic option -> thm
+  val prove_arity: theory -> string * sort list * class -> thm list
+    -> tactic option -> thm
+  val goal_subclass: theory -> class * class -> thm list
+  val goal_arity: theory -> string * sort list * class -> thm list
+  end;
 
-functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC
-  sharing Goals.Tactical = Tactic.Tactical): AX_CLASS =
+structure AxClass : AX_CLASS =
 struct
 
-structure Tactical = Goals.Tactical;
-structure Thm = Tactical.Thm;
-structure Sign = Thm.Sign;
-structure Type = Sign.Type;
-structure Pretty = Sign.Syntax.Pretty;
-
-open Logic Thm Tactical Tactic Goals;
-
-
 (** utilities **)
 
 (* type vars *)
@@ -63,7 +50,7 @@
 
 val get_axioms = mapfilter o get_ax;
 
-val is_def = is_equals o #prop o rep_thm;
+val is_def = Logic.is_equals o #prop o rep_thm;
 
 fun witnesses thy axms thms =
   map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));
@@ -74,13 +61,14 @@
 
 (* subclass relations as terms *)
 
-fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2);
+fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2);
 
 fun dest_classrel tm =
   let
     fun err () = raise_term "dest_classrel" [tm];
 
-    val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
+    val (ty, c2) = Logic.dest_inclass (Logic.freeze_vars tm)
+	           handle TERM _ => err ();
     val c1 = (case ty of TFree (_, [c]) => c | _ => err ());
   in
     (c1, c2)
@@ -94,14 +82,15 @@
     val names = tl (variantlist (replicate (length ss + 1) "'", []));
     val tfrees = map TFree (names ~~ ss);
   in
-    mk_inclass (Type (t, tfrees), c)
+    Logic.mk_inclass (Type (t, tfrees), c)
   end;
 
 fun dest_arity tm =
   let
     fun err () = raise_term "dest_arity" [tm];
 
-    val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
+    val (ty, c) = Logic.dest_inclass (Logic.freeze_vars tm) 
+	          handle TERM _ => err ();
     val (t, tfrees) =
       (case ty of
         Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys)
@@ -189,7 +178,7 @@
 
     fun abs_axm ax =
       if null (term_tfrees ax) then
-        mk_implies (mk_inclass (aT logicS, class), ax)
+        Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax)
       else
         map_term_tfrees (K (aT [class])) ax;
 
@@ -212,10 +201,10 @@
 
     val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
 
-    val int_axm = close_form o map_term_tfrees (K (aT axS));
-    fun inclass c = mk_inclass (aT axS, c);
+    val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
+    fun inclass c = Logic.mk_inclass (aT axS, c);
 
-    val intro_axm = list_implies
+    val intro_axm = Logic.list_implies
       (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   in
     add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy