src/Pure/drule.ML
changeset 1499 01fdd1ea6324
parent 1460 5a6f2aabd538
child 1596 4a09f4698813
     1.1 --- a/src/Pure/drule.ML	Fri Feb 16 11:35:52 1996 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Feb 16 12:08:49 1996 +0100
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  signature DRULE =
     1.6    sig
     1.7 -  structure Thm : THM
     1.8 -  local open Thm  in
     1.9    val add_defs		: (string * string) list -> theory -> theory
    1.10    val add_defs_i	: (string * term) list -> theory -> theory
    1.11    val asm_rl		: thm
    1.12 @@ -43,7 +41,7 @@
    1.13    val pprint_ctyp	: ctyp -> pprint_args -> unit
    1.14    val pprint_theory	: theory -> pprint_args -> unit
    1.15    val pprint_thm	: thm -> pprint_args -> unit
    1.16 -  val pretty_thm	: thm -> Sign.Syntax.Pretty.T
    1.17 +  val pretty_thm	: thm -> Pretty.T
    1.18    val print_cterm	: cterm -> unit
    1.19    val print_ctyp	: ctyp -> unit
    1.20    val print_goals	: int -> thm -> unit
    1.21 @@ -83,21 +81,11 @@
    1.22    val triv_forall_equality: thm
    1.23    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    1.24    val zero_var_indexes	: thm -> thm
    1.25 -  end
    1.26    end;
    1.27  
    1.28  
    1.29 -functor DruleFun (structure Logic: LOGIC and Thm: THM): DRULE =
    1.30 +structure Drule : DRULE =
    1.31  struct
    1.32 -structure Thm = Thm;
    1.33 -structure Sign = Thm.Sign;
    1.34 -structure Type = Sign.Type;
    1.35 -structure Syntax = Sign.Syntax;
    1.36 -structure Pretty = Syntax.Pretty
    1.37 -structure Symtab = Sign.Symtab;
    1.38 -
    1.39 -local open Thm
    1.40 -in
    1.41  
    1.42  (**** Extend Theories ****)
    1.43  
    1.44 @@ -824,6 +812,6 @@
    1.45                             (implies_intr V  (forall_intr x (assume V))))
    1.46    end;
    1.47  
    1.48 -end
    1.49  end;
    1.50  
    1.51 +open Drule;