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

diff -r 7b7d20e89b1b -r 01fdd1ea6324 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Feb 16 11:35:52 1996 +0100
+++ b/src/Pure/drule.ML	Fri Feb 16 12:08:49 1996 +0100
@@ -10,8 +10,6 @@
 
 signature DRULE =
   sig
-  structure Thm : THM
-  local open Thm  in
   val add_defs		: (string * string) list -> theory -> theory
   val add_defs_i	: (string * term) list -> theory -> theory
   val asm_rl		: thm
@@ -43,7 +41,7 @@
   val pprint_ctyp	: ctyp -> pprint_args -> unit
   val pprint_theory	: theory -> pprint_args -> unit
   val pprint_thm	: thm -> pprint_args -> unit
-  val pretty_thm	: thm -> Sign.Syntax.Pretty.T
+  val pretty_thm	: thm -> Pretty.T
   val print_cterm	: cterm -> unit
   val print_ctyp	: ctyp -> unit
   val print_goals	: int -> thm -> unit
@@ -83,21 +81,11 @@
   val triv_forall_equality: thm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val zero_var_indexes	: thm -> thm
-  end
   end;
 
 
-functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
+structure Drule : DRULE =
 struct
-structure Thm = Thm;
-structure Sign = Thm.Sign;
-structure Type = Sign.Type;
-structure Syntax = Sign.Syntax;
-structure Pretty = Syntax.Pretty
-structure Symtab = Sign.Symtab;
-
-local open Thm
-in
 
 (**** Extend Theories ****)
 
@@ -824,6 +812,6 @@
                            (implies_intr V  (forall_intr x (assume V))))
   end;
 
-end
 end;
 
+open Drule;