always unconstrain thm proofs;
authorwenzelm
Wed Jun 02 21:39:35 2010 +0200 (2010-06-02 ago)
changeset 37297a1acd424645a
parent 37296 1fad5b94c0ae
child 37298 1f3ca94ccb84
always unconstrain thm proofs;
src/Pure/Proof/reconstruct.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Jun 02 21:12:28 2010 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Jun 02 21:39:35 2010 +0200
     1.3 @@ -140,8 +140,7 @@
     1.4                | SOME Ts => (Ts, env));
     1.5              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
     1.6                (forall_intr_vfs prop) handle Library.UnequalLengths =>
     1.7 -                error ("Wrong number of type arguments for " ^
     1.8 -                  quote (get_name [] prop prf))
     1.9 +                error ("Wrong number of type arguments for " ^ quote (guess_name prf))
    1.10            in (prop', change_type (SOME Ts) prf, [], env', vTs) end;
    1.11  
    1.12      fun head_norm (prop, prf, cnstrts, env, vTs) =
     2.1 --- a/src/Pure/proofterm.ML	Wed Jun 02 21:12:28 2010 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Wed Jun 02 21:39:35 2010 +0200
     2.3 @@ -136,13 +136,11 @@
     2.4  
     2.5    val promise_proof: theory -> serial -> term -> proof
     2.6    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
     2.7 -  val unconstrain_thm_proofs: bool Unsynchronized.ref
     2.8    val thm_proof: theory -> string -> sort list -> term list -> term ->
     2.9      (serial * proof_body future) list -> proof_body -> pthm * proof
    2.10    val unconstrain_thm_proof: theory -> sort list -> term ->
    2.11      (serial * proof_body future) list -> proof_body -> pthm * proof
    2.12 -  val get_name: term list -> term -> proof -> string
    2.13 -  val get_name_unconstrained: sort list -> term list -> term -> proof -> string
    2.14 +  val get_name: sort list -> term list -> term -> proof -> string
    2.15    val guess_name: proof -> string
    2.16  end
    2.17  
    2.18 @@ -1422,7 +1420,7 @@
    2.19  
    2.20  (***** theorems *****)
    2.21  
    2.22 -fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
    2.23 +fun prepare_thm_proof thy name shyps hyps concl promises body =
    2.24    let
    2.25      val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
    2.26      val prop = Logic.list_implies (hyps, concl);
    2.27 @@ -1431,18 +1429,12 @@
    2.28          if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
    2.29        map SOME (frees_of prop);
    2.30  
    2.31 -    val (postproc, ofclasses, prop1, args1) =
    2.32 -      if do_unconstrain then
    2.33 -        let
    2.34 -          val ((atyp_map, constraints, outer_constraints), prop1) =
    2.35 -            Logic.unconstrainT shyps prop;
    2.36 -          val postproc = unconstrainT_body thy (atyp_map, constraints);
    2.37 -          val args1 =
    2.38 -            (map o Option.map o Term.map_types o Term.map_atyps)
    2.39 -              (Type.strip_sorts o atyp_map) args;
    2.40 -        in (postproc, map OfClass outer_constraints, prop1, args1) end
    2.41 -      else (I, [], prop, args);
    2.42 -    val argsP = ofclasses @ map Hyp hyps;
    2.43 +    val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
    2.44 +    val postproc = unconstrainT_body thy (atyp_map, constraints);
    2.45 +    val args1 =
    2.46 +      (map o Option.map o Term.map_types o Term.map_atyps)
    2.47 +        (Type.strip_sorts o atyp_map) args;
    2.48 +    val argsP = map OfClass outer_constraints @ map Hyp hyps;
    2.49  
    2.50      fun full_proof0 () =
    2.51        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    2.52 @@ -1464,28 +1456,17 @@
    2.53      val head = PThm (i, ((name, prop1, NONE), body'));
    2.54    in ((i, (name, prop1, body')), head, args, argsP, args1) end;
    2.55  
    2.56 -val unconstrain_thm_proofs = Unsynchronized.ref true;
    2.57 -
    2.58  fun thm_proof thy name shyps hyps concl promises body =
    2.59 -  let val (pthm, head, args, argsP, _) =
    2.60 -    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
    2.61 +  let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
    2.62    in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
    2.63  
    2.64  fun unconstrain_thm_proof thy shyps concl promises body =
    2.65    let
    2.66 -    val (pthm, head, _, _, args) =
    2.67 -      prepare_thm_proof true thy "" shyps [] concl promises body
    2.68 +    val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
    2.69    in (pthm, proof_combt' (head, args)) end;
    2.70  
    2.71  
    2.72 -fun get_name hyps prop prf =
    2.73 -  let val prop = Logic.list_implies (hyps, prop) in
    2.74 -    (case strip_combt (fst (strip_combP prf)) of
    2.75 -      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
    2.76 -    | _ => "")
    2.77 -  end;
    2.78 -
    2.79 -fun get_name_unconstrained shyps hyps prop prf =
    2.80 +fun get_name shyps hyps prop prf =
    2.81    let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
    2.82      (case strip_combt (fst (strip_combP prf)) of
    2.83        (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
     3.1 --- a/src/Pure/thm.ML	Wed Jun 02 21:12:28 2010 +0200
     3.2 +++ b/src/Pure/thm.ML	Wed Jun 02 21:39:35 2010 +0200
     3.3 @@ -584,8 +584,8 @@
     3.4  
     3.5  (* closed derivations with official name *)
     3.6  
     3.7 -fun derivation_name thm =
     3.8 -  Pt.guess_name (Pt.proof_of (raw_body thm));   (* FIXME tmp *)
     3.9 +fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
    3.10 +  Pt.get_name shyps hyps prop (Pt.proof_of body);
    3.11  
    3.12  fun name_derivation name (thm as Thm (der, args)) =
    3.13    let