src/Pure/Isar/element.ML
changeset 20150 baa589c574ff
parent 20068 19c7361db4a3
child 20218 be3bfb0699ba
     1.1 --- a/src/Pure/Isar/element.ML	Tue Jul 18 20:01:45 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Jul 18 20:01:46 2006 +0200
     1.3 @@ -216,45 +216,38 @@
     1.4  
     1.5  fun obtain prop ctxt =
     1.6    let
     1.7 -    val xs = Variable.rename_wrt ctxt [] (Logic.strip_params prop);
     1.8 -    val args = rev (map Free xs);
     1.9 -    val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
    1.10 -    val ctxt' = ctxt |> fold Variable.declare_term args;
    1.11 -  in (("", (map (apsnd SOME) xs, As)), ctxt') end;
    1.12 +    val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
    1.13 +    val As = Logic.strip_imp_prems (Thm.term_of prop');
    1.14 +    fun var (x, T) = (ProofContext.revert_skolem ctxt' x, SOME T);
    1.15 +  in (("", (map var xs, As)), ctxt') end;
    1.16  
    1.17  in
    1.18  
    1.19  fun pretty_statement ctxt kind raw_th =
    1.20    let
    1.21      val thy = ProofContext.theory_of ctxt;
    1.22 +    val cert = Thm.cterm_of thy;
    1.23 +
    1.24      val th = Goal.norm_hhf raw_th;
    1.25 +    val is_elim = ObjectLogic.is_elim th;
    1.26  
    1.27 -    fun standard_thesis t =
    1.28 -      let
    1.29 -        val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
    1.30 -        val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C);
    1.31 -      in Term.subst_atomic [(C, C')] t end;
    1.32 -
    1.33 -    val raw_prop =
    1.34 -      Thm.prop_of th
    1.35 -      |> singleton (Variable.monomorphic ctxt)
    1.36 -      |> K (ObjectLogic.is_elim th) ? standard_thesis
    1.37 -      |> Term.zero_var_indexes;
    1.38 +    val ([th'], ctxt') = Variable.import true [th] ctxt;
    1.39 +    val prop = Thm.prop_of th';
    1.40 +    val (prems, concl) = Logic.strip_horn prop;
    1.41 +    val concl_term = ObjectLogic.drop_judgment thy concl;
    1.42  
    1.43 -    val vars = Term.add_vars raw_prop [];
    1.44 -    val frees = Variable.rename_wrt ctxt [raw_prop] (map (apfst fst) vars);
    1.45 -    val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
    1.46 -
    1.47 -    val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
    1.48 -    val (prems, concl) = Logic.strip_horn prop;
    1.49 -    val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN;
    1.50 -    val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
    1.51 +    val fixes = fold_aterms (fn v as Free (x, T) =>
    1.52 +        if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    1.53 +        then insert (op =) (x, T) else I | _ => I) prop []
    1.54 +      |> rev |> map (apfst (ProofContext.revert_skolem ctxt'));
    1.55 +    val (assumes, cases) = take_suffix (fn prem =>
    1.56 +      is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    1.57    in
    1.58 -    pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
    1.59 -    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
    1.60 -    pretty_stmt ctxt
    1.61 +    pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
    1.62 +    pretty_ctxt ctxt' (Assumes (map (fn t => (("", []), [(t, [])])) assumes)) @
    1.63 +    pretty_stmt ctxt'
    1.64       (if null cases then Shows [(("", []), [(concl, [])])]
    1.65 -      else Obtains (#1 (fold_map obtain cases (ctxt |> Variable.declare_term prop))))
    1.66 +      else Obtains (#1 (fold_map (obtain o cert) cases ctxt')))
    1.67    end |> thm_name kind raw_th;
    1.68  
    1.69  end;