# HG changeset patch
# User wenzelm
# Date 1256661240 -3600
# Node ID 17014b1b9353426ab17e838d8311571ded421adf
# Parent  99577c7085c8e9c89ef237949ec49362a246279a
normalized basic type abbreviations;

diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -28,8 +28,8 @@
   val goal_thm_of : Proof.state -> thm
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
-  val theorems_in_proof_term : Thm.thm -> Thm.thm list
-  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
+  val theorems_in_proof_term : thm -> thm list
+  val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string
   val get_int_setting : (string * string) list -> string * int -> int
   val cpu_time : ('a -> 'b) -> 'a -> 'b * int
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -14,8 +14,8 @@
 signature SMT_NORMALIZE =
 sig
   val normalize_rule: Proof.context -> thm -> thm
-  val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm
-  val discharge_definition: Thm.cterm -> thm -> thm
+  val instantiate_free: cterm * cterm -> thm -> thm
+  val discharge_definition: cterm -> thm -> thm
 
   val trivial_let: Proof.context -> thm list -> thm list
   val positive_numerals: Proof.context -> thm list -> thm list
@@ -33,8 +33,7 @@
     AddFunUpdRules |
     AddAbsMinMaxRules
 
-  val normalize: config list -> Proof.context -> thm list ->
-    Thm.cterm list * thm list
+  val normalize: config list -> Proof.context -> thm list -> cterm list * thm list
 
   val setup: theory -> theory
 end
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -48,7 +48,7 @@
 
 datatype context = Context of {
   Ttab: typ Symtab.table,
-  ttab: Thm.cterm Symtab.table,
+  ttab: cterm Symtab.table,
   etab: T.preterm Inttab.table,
   ptab: R.proof Inttab.table,
   nctxt: Name.context }
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -13,7 +13,7 @@
 
   (*proof reconstruction*)
   type proof
-  val make_proof: rule -> int list -> Thm.cterm * Thm.cterm list -> proof
+  val make_proof: rule -> int list -> cterm * cterm list -> proof
   val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
     thm
 
@@ -103,11 +103,11 @@
   Unproved of {
     rule: rule,
     subs: int list,
-    prop: Thm.cterm,
-    vars: Thm.cterm list } |
+    prop: cterm,
+    vars: cterm list } |
   Sequent of {
-    hyps: Thm.cterm list,
-    vars: Thm.cterm list,
+    hyps: cterm list,
+    vars: cterm list,
     thm: theorem }
 
 fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs}
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/SMT/Tools/z3_proof_terms.ML
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -6,15 +6,15 @@
 
 signature Z3_PROOF_TERMS =
 sig
-  val mk_prop: Thm.cterm -> Thm.cterm
-  val mk_meta_eq: Thm.cterm -> Thm.cterm -> Thm.cterm
+  val mk_prop: cterm -> cterm
+  val mk_meta_eq: cterm -> cterm -> cterm
 
   type preterm
 
-  val compile: theory -> Name.context -> preterm -> Thm.cterm * Thm.cterm list
+  val compile: theory -> Name.context -> preterm -> cterm * cterm list
 
   val mk_bound: theory -> int -> typ -> preterm
-  val mk_fun: Thm.cterm -> preterm list -> preterm
+  val mk_fun: cterm -> preterm list -> preterm
   val mk_forall: theory -> string * typ -> preterm -> preterm
   val mk_exists: theory -> string * typ -> preterm -> preterm
 
@@ -73,8 +73,8 @@
 
 
 datatype preterm = Preterm of {
-  cterm: Thm.cterm,
-  vars: (int * Thm.cterm) list }
+  cterm: cterm,
+  vars: (int * cterm) list }
 
 fun mk_preterm (ct, vs) = Preterm {cterm=ct, vars=vs}
 fun dest_preterm (Preterm {cterm, vars}) = (cterm, vars)
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -74,7 +74,7 @@
   val get_rec_types : descr -> (string * sort) list -> typ list
   val interpret_construction : descr -> (string * sort) list
     -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
-    -> ((string * Term.typ list) * (string * 'a list) list) list
+    -> ((string * typ list) * (string * 'a list) list) list
   val check_nonempty : descr list -> unit
   val unfold_datatypes : 
     theory -> descr -> (string * sort) list -> info Symtab.table ->
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -589,7 +589,7 @@
 (* ------------------------------------------------------------------------- *)
 
 type logic_map =
-  {axioms : (Metis.Thm.thm * Thm.thm) list,
+  {axioms : (Metis.Thm.thm * thm) list,
    tfrees : ResClause.type_literal list};
 
 fun const_in_metis c (pred, tm_list) =
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -37,9 +37,9 @@
 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
 
 	(* propositional representation of HOL terms *)
-	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
+	val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table
 	(* HOL term representation of propositional formulae *)
-	val term_of_prop_formula : prop_formula -> Term.term
+	val term_of_prop_formula : prop_formula -> term
 end;
 
 structure PropLogic : PROP_LOGIC =
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -8,7 +8,7 @@
   type seed = Random_Engine.seed
   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-    -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
+    -> seed -> (('a -> 'b) * (unit -> term)) * seed
   val ensure_random_typecopy: string -> theory -> theory
   val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
   val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -25,16 +25,15 @@
 
   exception MAXVARS_EXCEEDED
 
-  val add_interpreter : string -> (theory -> model -> arguments -> Term.term ->
+  val add_interpreter : string -> (theory -> model -> arguments -> term ->
     (interpretation * model * arguments) option) -> theory -> theory
-  val add_printer     : string -> (theory -> model -> Term.typ ->
-    interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
+  val add_printer     : string -> (theory -> model -> typ ->
+    interpretation -> (int -> bool) -> term option) -> theory -> theory
 
-  val interpret : theory -> model -> arguments -> Term.term ->
+  val interpret : theory -> model -> arguments -> term ->
     (interpretation * model * arguments)
 
-  val print       : theory -> model -> Term.typ -> interpretation ->
-    (int -> bool) -> Term.term
+  val print       : theory -> model -> typ -> interpretation -> (int -> bool) -> term
   val print_model : theory -> model -> (int -> bool) -> string
 
 (* ------------------------------------------------------------------------- *)
@@ -46,10 +45,10 @@
   val get_default_params : theory -> (string * string) list
   val actual_params      : theory -> (string * string) list -> params
 
-  val find_model : theory -> params -> Term.term -> bool -> unit
+  val find_model : theory -> params -> term -> bool -> unit
 
   (* tries to find a model for a formula: *)
-  val satisfy_term   : theory -> (string * string) list -> Term.term -> unit
+  val satisfy_term   : theory -> (string * string) list -> term -> unit
   (* tries to find a model that refutes a formula: *)
   val refute_term : theory -> (string * string) list -> term -> unit
   val refute_goal : theory -> (string * string) list -> thm -> int -> unit
@@ -60,20 +59,18 @@
 (* Additional functions used by Nitpick (to be factored out)                 *)
 (* ------------------------------------------------------------------------- *)
 
-  val close_form : Term.term -> Term.term
-  val get_classdef : theory -> string -> (string * Term.term) option
-  val norm_rhs : Term.term -> Term.term
-  val get_def : theory -> string * Term.typ -> (string * Term.term) option
-  val get_typedef : theory -> Term.typ -> (string * Term.term) option
-  val is_IDT_constructor : theory -> string * Term.typ -> bool
-  val is_IDT_recursor : theory -> string * Term.typ -> bool
-  val is_const_of_class: theory -> string * Term.typ -> bool
-  val monomorphic_term : Type.tyenv -> Term.term -> Term.term
-  val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
-  val string_of_typ : Term.typ -> string
-  val typ_of_dtyp :
-    Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
-    -> Term.typ
+  val close_form : term -> term
+  val get_classdef : theory -> string -> (string * term) option
+  val norm_rhs : term -> term
+  val get_def : theory -> string * typ -> (string * term) option
+  val get_typedef : theory -> typ -> (string * term) option
+  val is_IDT_constructor : theory -> string * typ -> bool
+  val is_IDT_recursor : theory -> string * typ -> bool
+  val is_const_of_class: theory -> string * typ -> bool
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
+  val string_of_typ : typ -> string
+  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
 end;  (* signature REFUTE *)
 
 structure Refute : REFUTE =
@@ -185,7 +182,7 @@
 (* ------------------------------------------------------------------------- *)
 
   type model =
-    (Term.typ * int) list * (Term.term * interpretation) list;
+    (typ * int) list * (term * interpretation) list;
 
 (* ------------------------------------------------------------------------- *)
 (* arguments: additional arguments required during interpretation of terms   *)
@@ -207,10 +204,10 @@
   structure RefuteData = TheoryDataFun
   (
     type T =
-      {interpreters: (string * (theory -> model -> arguments -> Term.term ->
+      {interpreters: (string * (theory -> model -> arguments -> term ->
         (interpretation * model * arguments) option)) list,
-       printers: (string * (theory -> model -> Term.typ -> interpretation ->
-        (int -> bool) -> Term.term option)) list,
+       printers: (string * (theory -> model -> typ -> interpretation ->
+        (int -> bool) -> term option)) list,
        parameters: string Symtab.table};
     val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
     val copy = I;
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -10,17 +10,17 @@
   val fix_sorts: sort Vartab.table -> term -> term
   val invert_const: string -> string
   val invert_type_const: string -> string
-  val num_typargs: Context.theory -> string -> int
+  val num_typargs: theory -> string -> int
   val make_tvar: string -> typ
   val strip_prefix: string -> string -> string option
-  val setup: Context.theory -> Context.theory
+  val setup: theory -> theory
   (* extracting lemma list*)
   val find_failure: string -> string option
   val lemma_list: bool -> string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
+    string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   (* structured proofs *)
   val structured_proof: string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
+    string * string vector * (int * int) * Proof.context * thm * int -> string * string list
 end;
 
 structure ResReconstruct : RES_RECONSTRUCT =
diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -92,8 +92,8 @@
 (* ------------------------------------------------------------------------- *)
 
 datatype CLAUSE = NO_CLAUSE
-                | ORIG_CLAUSE of Thm.thm
-                | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list;
+                | ORIG_CLAUSE of thm
+                | RAW_CLAUSE of thm * (int * cterm) list;
 
 (* ------------------------------------------------------------------------- *)
 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
diff -r 99577c7085c8 -r 17014b1b9353 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/Tools/eqsubst.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -269,7 +269,7 @@
 (* FOR DEBUGGING...
 type trace_subst_errT = int (* subgoal *)
         * thm (* thm with all goals *)
-        * (Thm.cterm list (* certified free var placeholders for vars *)
+        * (cterm list (* certified free var placeholders for vars *)
            * thm)  (* trivial thm of goal concl *)
             (* possible matches/unifiers *)
         * thm (* rule *)