1.1 --- a/src/Provers/classical.ML	Sat Jan 15 18:49:42 2011 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Jan 15 20:51:22 2011 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  *)
     1.5  
     1.6  fun classical_rule rule =
     1.7 -  if Object_Logic.is_elim rule then
     1.8 +  if is_some (Object_Logic.elim_concl rule) then
     1.9      let
    1.10        val rule' = rule RS classical;
    1.11        val concl' = Thm.concl_of rule';

     2.1 --- a/src/Pure/Isar/element.ML	Sat Jan 15 18:49:42 2011 +0100
     2.2 +++ b/src/Pure/Isar/element.ML	Sat Jan 15 20:51:22 2011 +0100
     2.3 @@ -201,6 +201,16 @@
     2.4  
     2.5  local
     2.6  
     2.7 +fun standard_elim th =
     2.8 +  (case Object_Logic.elim_concl th of
     2.9 +    SOME C =>
    2.10 +      let
    2.11 +        val cert = Thm.cterm_of (Thm.theory_of_thm th);
    2.12 +        val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
    2.13 +        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
    2.14 +      in (th', true) end
    2.15 +  | NONE => (th, false));
    2.16 +
    2.17  fun thm_name kind th prts =
    2.18    let val head =
    2.19      if Thm.has_name_hint th then
    2.20 @@ -209,13 +219,13 @@
    2.21      else Pretty.command kind
    2.22    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
    2.23  
    2.24 -fun fix (x, T) = (Binding.name x, SOME T);
    2.25 -
    2.26  fun obtain prop ctxt =
    2.27    let
    2.28 -    val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
    2.29 +    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
    2.30 +    fun fix (x, T) = (Binding.name (ProofContext.revert_skolem ctxt' x), SOME T);
    2.31 +    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
    2.32      val As = Logic.strip_imp_prems (Thm.term_of prop');
    2.33 -  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
    2.34 +  in ((Binding.empty, (xs, As)), ctxt') end;
    2.35  
    2.36  in
    2.37  
    2.38 @@ -224,17 +234,15 @@
    2.39      val thy = ProofContext.theory_of ctxt;
    2.40      val cert = Thm.cterm_of thy;
    2.41  
    2.42 -    val th = Raw_Simplifier.norm_hhf raw_th;
    2.43 -    val is_elim = Object_Logic.is_elim th;
    2.44 -
    2.45 -    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
    2.46 +    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
    2.47 +    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
    2.48      val prop = Thm.prop_of th';
    2.49      val (prems, concl) = Logic.strip_horn prop;
    2.50      val concl_term = Object_Logic.drop_judgment thy concl;
    2.51  
    2.52      val fixes = fold_aterms (fn v as Free (x, T) =>
    2.53          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    2.54 -        then insert (op =) (x, T) else I | _ => I) prop [] |> rev;
    2.55 +        then insert (op =) (ProofContext.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
    2.56      val (assumes, cases) = take_suffix (fn prem =>
    2.57        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    2.58    in

     3.1 --- a/src/Pure/Isar/object_logic.ML	Sat Jan 15 18:49:42 2011 +0100
     3.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jan 15 20:51:22 2011 +0100
     3.3 @@ -17,7 +17,7 @@
     3.4    val ensure_propT: theory -> term -> term
     3.5    val dest_judgment: cterm -> cterm
     3.6    val judgment_conv: conv -> conv
     3.7 -  val is_elim: thm -> bool
     3.8 +  val elim_concl: thm -> term option
     3.9    val declare_atomize: attribute
    3.10    val declare_rulify: attribute
    3.11    val atomize_term: theory -> term -> term
    3.12 @@ -145,13 +145,15 @@
    3.13  
    3.14  (* elimination rules *)
    3.15  
    3.16 -fun is_elim rule =
    3.17 +fun elim_concl rule =
    3.18    let
    3.19      val thy = Thm.theory_of_thm rule;
    3.20      val concl = Thm.concl_of rule;
    3.21 +    val C = drop_judgment thy concl;
    3.22    in
    3.23 -    Term.is_Var (drop_judgment thy concl) andalso
    3.24 +    if Term.is_Var C andalso
    3.25        exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
    3.26 +    then SOME C else NONE
    3.27    end;
    3.28  
    3.29