1.1 --- a/src/Pure/proofterm.ML	Thu May 13 21:17:09 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu May 13 21:36:38 2010 +0200
     1.3 @@ -132,7 +132,8 @@
     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 thm_proof: theory -> string -> term list -> term ->
     1.8 +  val unconstrain_thm_proofs: bool Unsynchronized.ref
     1.9 +  val thm_proof: theory -> string -> sort list -> term list -> term ->
    1.10      (serial * proof_body future) list -> proof_body -> pthm * proof
    1.11    val get_name: term list -> term -> proof -> string
    1.12    val get_name_unconstrained: sort list -> term list -> term -> proof -> string
    1.13 @@ -1373,22 +1374,22 @@
    1.14      val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
    1.15    in PBody {oracles = oracles, thms = thms, proof = proof} end;
    1.16  
    1.17 -fun fulfill_proof_future _ [] body = Future.value body
    1.18 -  | fulfill_proof_future thy promises body =
    1.19 +fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
    1.20 +  | fulfill_proof_future thy promises postproc body =
    1.21        Future.fork_deps (map snd promises) (fn () =>
    1.22 -        fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
    1.23 +        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body));
    1.24  
    1.25  
    1.26  (***** abstraction over sort constraints *****)
    1.27  
    1.28 -fun unconstrainT_proof thy atyp_map constraints =
    1.29 +fun unconstrainT_prf thy (atyp_map, constraints) =
    1.30    let
    1.31      fun hyp_map hyp =
    1.32        (case AList.lookup (op =) constraints hyp of
    1.33          SOME t => Hyp t
    1.34 -      | NONE => raise Fail "unconstrainT_proof: missing constraint");
    1.35 +      | NONE => raise Fail "unconstrainT_prf: missing constraint");
    1.36  
    1.37 -    val typ = Type.strip_sorts o atyp_map;
    1.38 +    val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o atyp_map);
    1.39      fun ofclass (ty, c) =
    1.40        let val ty' = Term.map_atyps atyp_map ty;
    1.41        in the_single (of_sort_proof thy hyp_map (ty', [c])) end;
    1.42 @@ -1397,16 +1398,18 @@
    1.43      #> fold_rev (implies_intr_proof o snd) constraints
    1.44    end;
    1.45  
    1.46 -fun unconstrainT_body thy atyp_map constraints (PBody {oracles, thms, proof}) =
    1.47 +fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) =
    1.48    PBody
    1.49     {oracles = oracles,  (* FIXME unconstrain (!?!) *)
    1.50      thms = thms,
    1.51 -    proof = unconstrainT_proof thy atyp_map constraints proof};
    1.52 +    proof = unconstrainT_prf thy constrs proof};
    1.53  
    1.54  
    1.55  (***** theorems *****)
    1.56  
    1.57 -fun thm_proof thy name hyps concl promises body =
    1.58 +val unconstrain_thm_proofs = Unsynchronized.ref false;
    1.59 +
    1.60 +fun thm_proof thy name shyps hyps concl promises body =
    1.61    let
    1.62      val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
    1.63      val prop = Logic.list_implies (hyps, concl);
    1.64 @@ -1415,23 +1418,32 @@
    1.65          if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
    1.66        map SOME (frees_of prop);
    1.67  
    1.68 +    val (postproc, ofclasses, prop1) =
    1.69 +      if ! unconstrain_thm_proofs then
    1.70 +        let
    1.71 +          val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
    1.72 +          val postproc = unconstrainT_body thy (atyp_map, constraints);
    1.73 +        in (postproc, map (OfClass o fst) constraints, prop1) end
    1.74 +      else (I, [], prop);
    1.75 +    val argsP = ofclasses @ map Hyp hyps;
    1.76 +
    1.77      val proof0 =
    1.78        if ! proofs = 2 then
    1.79          #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    1.80        else MinProof;
    1.81      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.82  
    1.83 -    fun new_prf () = (serial (), fulfill_proof_future thy promises body0);
    1.84 +    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.85      val (i, body') =
    1.86        (case strip_combt (fst (strip_combP prf)) of
    1.87          (PThm (i, ((old_name, prop', NONE), body')), args') =>
    1.88 -          if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args'
    1.89 +          if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'
    1.90            then (i, body')
    1.91            else new_prf ()
    1.92        | _ => new_prf ());
    1.93 -    val head = PThm (i, ((name, prop, NONE), body'));
    1.94 +    val head = PThm (i, ((name, prop1, NONE), body'));
    1.95    in
    1.96 -    ((i, (name, prop, body')), proof_combP (proof_combt' (head, args), map Hyp hyps))
    1.97 +    ((i, (name, prop1, body')), proof_combP (proof_combt' (head, args), argsP))
    1.98    end;
    1.99  
   1.100  fun get_name hyps prop prf =

     2.1 --- a/src/Pure/thm.ML	Thu May 13 21:17:09 2010 +0200
     2.2 +++ b/src/Pure/thm.ML	Thu May 13 21:36:38 2010 +0200
     2.3 @@ -586,17 +586,17 @@
     2.4  (* closed derivations with official name *)
     2.5  
     2.6  fun derivation_name thm =
     2.7 -  Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
     2.8 +  Pt.guess_name (Pt.proof_of (raw_body thm));   (* FIXME tmp *)
     2.9  
    2.10  fun name_derivation name (thm as Thm (der, args)) =
    2.11    let
    2.12      val Deriv {promises, body} = der;
    2.13 -    val {thy_ref, hyps, prop, tpairs, ...} = args;
    2.14 +    val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;
    2.15      val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
    2.16  
    2.17      val ps = map (apsnd (Future.map proof_body_of)) promises;
    2.18      val thy = Theory.deref thy_ref;
    2.19 -    val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
    2.20 +    val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body;
    2.21      val der' = make_deriv [] [] [pthm] proof;
    2.22      val _ = Theory.check_thy thy;
    2.23    in Thm (der', args) end;