# HG changeset patch
# User wenzelm
# Date 1275507575 -7200
# Node ID a1acd424645a73918075bb1d3887a4b411529d7b
# Parent  1fad5b94c0ae230f1c6395fa7627006ede9995d3
always unconstrain thm proofs;

diff -r 1fad5b94c0ae -r a1acd424645a src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Jun 02 21:12:28 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Jun 02 21:39:35 2010 +0200
@@ -140,8 +140,7 @@
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
               (forall_intr_vfs prop) handle Library.UnequalLengths =>
-                error ("Wrong number of type arguments for " ^
-                  quote (get_name [] prop prf))
+                error ("Wrong number of type arguments for " ^ quote (guess_name prf))
           in (prop', change_type (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
diff -r 1fad5b94c0ae -r a1acd424645a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jun 02 21:12:28 2010 +0200
+++ b/src/Pure/proofterm.ML	Wed Jun 02 21:39:35 2010 +0200
@@ -136,13 +136,11 @@
 
   val promise_proof: theory -> serial -> term -> proof
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val unconstrain_thm_proofs: bool Unsynchronized.ref
   val thm_proof: theory -> string -> sort list -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val unconstrain_thm_proof: theory -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
-  val get_name: term list -> term -> proof -> string
-  val get_name_unconstrained: sort list -> term list -> term -> proof -> string
+  val get_name: sort list -> term list -> term -> proof -> string
   val guess_name: proof -> string
 end
 
@@ -1422,7 +1420,7 @@
 
 (***** theorems *****)
 
-fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
+fun prepare_thm_proof thy name shyps hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val prop = Logic.list_implies (hyps, concl);
@@ -1431,18 +1429,12 @@
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
       map SOME (frees_of prop);
 
-    val (postproc, ofclasses, prop1, args1) =
-      if do_unconstrain then
-        let
-          val ((atyp_map, constraints, outer_constraints), prop1) =
-            Logic.unconstrainT shyps prop;
-          val postproc = unconstrainT_body thy (atyp_map, constraints);
-          val args1 =
-            (map o Option.map o Term.map_types o Term.map_atyps)
-              (Type.strip_sorts o atyp_map) args;
-        in (postproc, map OfClass outer_constraints, prop1, args1) end
-      else (I, [], prop, args);
-    val argsP = ofclasses @ map Hyp hyps;
+    val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
+    val postproc = unconstrainT_body thy (atyp_map, constraints);
+    val args1 =
+      (map o Option.map o Term.map_types o Term.map_atyps)
+        (Type.strip_sorts o atyp_map) args;
+    val argsP = map OfClass outer_constraints @ map Hyp hyps;
 
     fun full_proof0 () =
       #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
@@ -1464,28 +1456,17 @@
     val head = PThm (i, ((name, prop1, NONE), body'));
   in ((i, (name, prop1, body')), head, args, argsP, args1) end;
 
-val unconstrain_thm_proofs = Unsynchronized.ref true;
-
 fun thm_proof thy name shyps hyps concl promises body =
-  let val (pthm, head, args, argsP, _) =
-    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
+  let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
   in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
 
 fun unconstrain_thm_proof thy shyps concl promises body =
   let
-    val (pthm, head, _, _, args) =
-      prepare_thm_proof true thy "" shyps [] concl promises body
+    val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
   in (pthm, proof_combt' (head, args)) end;
 
 
-fun get_name hyps prop prf =
-  let val prop = Logic.list_implies (hyps, prop) in
-    (case strip_combt (fst (strip_combP prf)) of
-      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
-    | _ => "")
-  end;
-
-fun get_name_unconstrained shyps hyps prop prf =
+fun get_name shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case strip_combt (fst (strip_combP prf)) of
       (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
diff -r 1fad5b94c0ae -r a1acd424645a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jun 02 21:12:28 2010 +0200
+++ b/src/Pure/thm.ML	Wed Jun 02 21:39:35 2010 +0200
@@ -584,8 +584,8 @@
 
 (* closed derivations with official name *)
 
-fun derivation_name thm =
-  Pt.guess_name (Pt.proof_of (raw_body thm));   (* FIXME tmp *)
+fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+  Pt.get_name shyps hyps prop (Pt.proof_of body);
 
 fun name_derivation name (thm as Thm (der, args)) =
   let