src/Pure/proofterm.ML
changeset 37297 a1acd424645a
parent 37251 72c7e636067b
child 39020 ac0f24f850c9
     1.1 --- a/src/Pure/proofterm.ML	Wed Jun 02 21:12:28 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Jun 02 21:39:35 2010 +0200
     1.3 @@ -136,13 +136,11 @@
     1.4  
     1.5    val promise_proof: theory -> serial -> term -> proof
     1.6    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
     1.7 -  val unconstrain_thm_proofs: bool Unsynchronized.ref
     1.8    val thm_proof: theory -> string -> sort list -> term list -> term ->
     1.9      (serial * proof_body future) list -> proof_body -> pthm * proof
    1.10    val unconstrain_thm_proof: theory -> sort list -> term ->
    1.11      (serial * proof_body future) list -> proof_body -> pthm * proof
    1.12 -  val get_name: term list -> term -> proof -> string
    1.13 -  val get_name_unconstrained: sort list -> term list -> term -> proof -> string
    1.14 +  val get_name: sort list -> term list -> term -> proof -> string
    1.15    val guess_name: proof -> string
    1.16  end
    1.17  
    1.18 @@ -1422,7 +1420,7 @@
    1.19  
    1.20  (***** theorems *****)
    1.21  
    1.22 -fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
    1.23 +fun prepare_thm_proof thy name shyps hyps concl promises body =
    1.24    let
    1.25      val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
    1.26      val prop = Logic.list_implies (hyps, concl);
    1.27 @@ -1431,18 +1429,12 @@
    1.28          if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
    1.29        map SOME (frees_of prop);
    1.30  
    1.31 -    val (postproc, ofclasses, prop1, args1) =
    1.32 -      if do_unconstrain then
    1.33 -        let
    1.34 -          val ((atyp_map, constraints, outer_constraints), prop1) =
    1.35 -            Logic.unconstrainT shyps prop;
    1.36 -          val postproc = unconstrainT_body thy (atyp_map, constraints);
    1.37 -          val args1 =
    1.38 -            (map o Option.map o Term.map_types o Term.map_atyps)
    1.39 -              (Type.strip_sorts o atyp_map) args;
    1.40 -        in (postproc, map OfClass outer_constraints, prop1, args1) end
    1.41 -      else (I, [], prop, args);
    1.42 -    val argsP = ofclasses @ map Hyp hyps;
    1.43 +    val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
    1.44 +    val postproc = unconstrainT_body thy (atyp_map, constraints);
    1.45 +    val args1 =
    1.46 +      (map o Option.map o Term.map_types o Term.map_atyps)
    1.47 +        (Type.strip_sorts o atyp_map) args;
    1.48 +    val argsP = map OfClass outer_constraints @ map Hyp hyps;
    1.49  
    1.50      fun full_proof0 () =
    1.51        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    1.52 @@ -1464,28 +1456,17 @@
    1.53      val head = PThm (i, ((name, prop1, NONE), body'));
    1.54    in ((i, (name, prop1, body')), head, args, argsP, args1) end;
    1.55  
    1.56 -val unconstrain_thm_proofs = Unsynchronized.ref true;
    1.57 -
    1.58  fun thm_proof thy name shyps hyps concl promises body =
    1.59 -  let val (pthm, head, args, argsP, _) =
    1.60 -    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
    1.61 +  let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
    1.62    in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
    1.63  
    1.64  fun unconstrain_thm_proof thy shyps concl promises body =
    1.65    let
    1.66 -    val (pthm, head, _, _, args) =
    1.67 -      prepare_thm_proof true thy "" shyps [] concl promises body
    1.68 +    val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
    1.69    in (pthm, proof_combt' (head, args)) end;
    1.70  
    1.71  
    1.72 -fun get_name hyps prop prf =
    1.73 -  let val prop = Logic.list_implies (hyps, prop) in
    1.74 -    (case strip_combt (fst (strip_combP prf)) of
    1.75 -      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
    1.76 -    | _ => "")
    1.77 -  end;
    1.78 -
    1.79 -fun get_name_unconstrained shyps hyps prop prf =
    1.80 +fun get_name shyps hyps prop prf =
    1.81    let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
    1.82      (case strip_combt (fst (strip_combP prf)) of
    1.83        (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""