1.1 --- a/src/Pure/Isar/element.ML	Sat Jan 15 18:49:42 2011 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Sat Jan 15 20:51:22 2011 +0100
     1.3 @@ -201,6 +201,16 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun standard_elim th =
     1.8 +  (case Object_Logic.elim_concl th of
     1.9 +    SOME C =>
    1.10 +      let
    1.11 +        val cert = Thm.cterm_of (Thm.theory_of_thm th);
    1.12 +        val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
    1.13 +        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
    1.14 +      in (th', true) end
    1.15 +  | NONE => (th, false));
    1.16 +
    1.17  fun thm_name kind th prts =
    1.18    let val head =
    1.19      if Thm.has_name_hint th then
    1.20 @@ -209,13 +219,13 @@
    1.21      else Pretty.command kind
    1.22    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
    1.23  
    1.24 -fun fix (x, T) = (Binding.name x, SOME T);
    1.25 -
    1.26  fun obtain prop ctxt =
    1.27    let
    1.28 -    val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
    1.29 +    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
    1.30 +    fun fix (x, T) = (Binding.name (ProofContext.revert_skolem ctxt' x), SOME T);
    1.31 +    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
    1.32      val As = Logic.strip_imp_prems (Thm.term_of prop');
    1.33 -  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
    1.34 +  in ((Binding.empty, (xs, As)), ctxt') end;
    1.35  
    1.36  in
    1.37  
    1.38 @@ -224,17 +234,15 @@
    1.39      val thy = ProofContext.theory_of ctxt;
    1.40      val cert = Thm.cterm_of thy;
    1.41  
    1.42 -    val th = Raw_Simplifier.norm_hhf raw_th;
    1.43 -    val is_elim = Object_Logic.is_elim th;
    1.44 -
    1.45 -    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
    1.46 +    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
    1.47 +    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
    1.48      val prop = Thm.prop_of th';
    1.49      val (prems, concl) = Logic.strip_horn prop;
    1.50      val concl_term = Object_Logic.drop_judgment thy concl;
    1.51  
    1.52      val fixes = fold_aterms (fn v as Free (x, T) =>
    1.53          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    1.54 -        then insert (op =) (x, T) else I | _ => I) prop [] |> rev;
    1.55 +        then insert (op =) (ProofContext.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
    1.56      val (assumes, cases) = take_suffix (fn prem =>
    1.57        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    1.58    in