# HG changeset patch
# User wenzelm
# Date 1425506185 -3600
# Node ID 6020e3dec7b5098c4b71082efa2004f59f6a81fb
# Parent  ddf6deaadfe872efba92dc3032eadd1b5cb26db4
removed unused;
tuned comments;

diff -r ddf6deaadfe8 -r 6020e3dec7b5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Mar 04 22:05:01 2015 +0100
+++ b/src/Pure/thm.ML	Wed Mar 04 22:56:25 2015 +0100
@@ -3,12 +3,12 @@
     Author:     Makarius
 
 The very core of Isabelle's Meta Logic: certified types and terms,
-derivations, theorems, framework rules (including lifting and
+derivations, theorems, inference rules (including lifting and
 resolution), oracles.
 *)
 
 signature BASIC_THM =
-  sig
+sig
   type ctyp
   type cterm
   exception CTERM of string * cterm list
@@ -20,17 +20,13 @@
 signature THM =
 sig
   include BASIC_THM
-
   (*certified types*)
-  val rep_ctyp: ctyp -> {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T}
   val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
   val ctyp_of: theory -> typ -> ctyp
   val dest_ctyp: ctyp -> ctyp list
-
   (*certified terms*)
   val rep_cterm: cterm -> {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}
-  val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
   val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val typ_of_cterm: cterm -> typ
@@ -50,7 +46,6 @@
   val incr_indexes_cterm: int -> cterm -> cterm
   val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
-
   (*theorems*)
   val rep_thm: thm ->
    {thy: theory,
@@ -102,7 +97,7 @@
   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   val norm_proof: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
-  (*meta rules*)
+  (*inference rules*)
   val assume: cterm -> thm
   val implies_intr: cterm -> thm -> thm
   val implies_elim: thm -> thm -> thm
@@ -140,6 +135,7 @@
   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+  (*oracles*)
   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
@@ -154,7 +150,6 @@
 abstype ctyp = Ctyp of {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T}
 with
 
-fun rep_ctyp (Ctyp args) = args;
 fun theory_of_ctyp (Ctyp {thy, ...}) = thy;
 fun typ_of (Ctyp {T, ...}) = T;
 
@@ -181,10 +176,6 @@
 
 fun rep_cterm (Cterm args) = args;
 
-fun crep_cterm (Cterm {thy, t, T, maxidx, sorts}) =
-  {thy = thy, t = t, maxidx = maxidx, sorts = sorts,
-    T = Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}};
-
 fun theory_of_cterm (Cterm {thy, ...}) = thy;
 fun term_of (Cterm {t, ...}) = t;