# HG changeset patch
# User wenzelm
# Date 1327497239 -3600
# Node ID 6fae74ee591a658c7b0c20c54897bd17c4f0bb09
# Parent  e18ccb00fb8ff41e003da55298b8b65b4e565fce
removed obscure/outdated material;

diff -r e18ccb00fb8f -r 6fae74ee591a doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Wed Jan 25 13:31:56 2012 +0100
+++ b/doc-src/Ref/thm.tex	Wed Jan 25 14:13:59 2012 +0100
@@ -193,13 +193,8 @@
 cprems_of     : thm -> cterm list
 nprems_of     : thm -> int
 tpairs_of     : thm -> (term*term) list
-sign_of_thm   : thm -> Sign.sg
 theory_of_thm : thm -> theory
 dest_state : thm * int -> (term*term) list * term list * term * term
-rep_thm    : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
-                     shyps: sort list, hyps: term list, prop: term\}
-crep_thm   : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
-                     shyps: sort list, hyps: cterm list, prop:{\ts}cterm\}
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
@@ -221,9 +216,6 @@
 \item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
   of $thm$.
   
-\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
-  associated with $thm$.
-  
 \item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
   with $thm$.  Note that this does a lookup in Isabelle's global
   database of loaded theories.
@@ -233,16 +225,6 @@
 list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
 (this will be an implication if there are more than $i$ subgoals).
 
-\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
-  containing the statement of~$thm$ ({\tt prop}), its list of
-  meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
-  on the maximum subscript of its unknowns ({\tt maxidx}), and a
-  reference to its signature ({\tt sign_ref}).  The {\tt shyps} field
-  is discussed below.
-  
-\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
-  the hypotheses and statement as certified terms.
-
 \end{ttdescription}
 
 
@@ -403,21 +385,6 @@
 Most of these rules have the sole purpose of implementing particular
 tactics.  There are few occasions for applying them directly to a theorem.
 
-\subsection{Proof by assumption}
-\index{meta-assumptions}
-\begin{ttbox} 
-assumption    : int -> thm -> thm Seq.seq
-eq_assumption : int -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{assumption} {\it i} $thm$] 
-attempts to solve premise~$i$ of~$thm$ by assumption.
-
-\item[\ttindexbold{eq_assumption}] 
-is like {\tt assumption} but does not use unification.
-\end{ttdescription}
-
-
 \subsection{Resolution}
 \index{resolution}
 \begin{ttbox} 
@@ -475,20 +442,9 @@
 
 \subsection{Other meta-rules}
 \begin{ttbox} 
-trivial            : cterm -> thm
-lift_rule          : (thm * int) -> thm -> thm
 rename_params_rule : string list * int -> thm -> thm
-flexflex_rule      : thm -> thm Seq.seq
 \end{ttbox}
 \begin{ttdescription}
-\item[\ttindexbold{trivial} $ct$] 
-makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
-This is the initial state for a goal-directed proof of~$\phi$.  The rule
-checks that $ct$ has type~$prop$.
-
-\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
-prepares $rule$ for resolution by lifting it over the parameters and
-assumptions of subgoal~$i$ of~$state$.
 
 \item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$] 
 uses the $names$ to rename the parameters of premise~$i$ of $thm$.  The
@@ -497,8 +453,6 @@
 ensure that all the parameters are distinct.
 \index{parameters!renaming}
 
-\item[\ttindexbold{flexflex_rule} $thm$]  \index{flex-flex constraints}
-removes all flex-flex pairs from $thm$ using the trivial unifier.
 \end{ttdescription}
 \index{meta-rules|)}
 
diff -r e18ccb00fb8f -r 6fae74ee591a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jan 25 13:31:56 2012 +0100
+++ b/src/Pure/thm.ML	Wed Jan 25 14:13:59 2012 +0100
@@ -1306,8 +1306,8 @@
     | _ => raise THM("dest_state", i, [state]))
   handle TERM _ => raise THM("dest_state", i, [state]);
 
-(*Increment variables and parameters of orule as required for
-  resolution with a goal.*)
+(*Prepare orule for resolution by lifting it over the parameters and
+assumptions of goal.*)
 fun lift_rule goal orule =
   let
     val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal;