merged

--- a/src/Provers/classical.ML	Sat Jan 15 20:05:29 2011 +0100
+++ b/src/Provers/classical.ML	Sat Jan 15 21:24:15 2011 +0100
@@ -153,7 +153,7 @@
 *)
 
 fun classical_rule rule =
-  if Object_Logic.is_elim rule then
+  if is_some (Object_Logic.elim_concl rule) then
     let
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';

--- a/src/Pure/Isar/element.ML	Sat Jan 15 20:05:29 2011 +0100
+++ b/src/Pure/Isar/element.ML	Sat Jan 15 21:24:15 2011 +0100
@@ -201,6 +201,16 @@
 
 local
 
+fun standard_elim th =
+  (case Object_Logic.elim_concl th of
+    SOME C =>
+      let
+        val cert = Thm.cterm_of (Thm.theory_of_thm th);
+        val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
+        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
+      in (th', true) end
+  | NONE => (th, false));
+
 fun thm_name kind th prts =
   let val head =
     if Thm.has_name_hint th then
@@ -209,13 +219,13 @@
     else Pretty.command kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
-fun fix (x, T) = (Binding.name x, SOME T);
-
 fun obtain prop ctxt =
   let
-    val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
+    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
+    fun fix (x, T) = (Binding.name (ProofContext.revert_skolem ctxt' x), SOME T);
+    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
     val As = Logic.strip_imp_prems (Thm.term_of prop');
-  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
+  in ((Binding.empty, (xs, As)), ctxt') end;
 
 in
 
@@ -224,17 +234,15 @@
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
-    val th = Raw_Simplifier.norm_hhf raw_th;
-    val is_elim = Object_Logic.is_elim th;
-
-    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
+    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
+    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
     val concl_term = Object_Logic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
         if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
-        then insert (op =) (x, T) else I | _ => I) prop [] |> rev;
+        then insert (op =) (ProofContext.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
     val (assumes, cases) = take_suffix (fn prem =>
       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
   in

--- a/src/Pure/Isar/object_logic.ML	Sat Jan 15 20:05:29 2011 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sat Jan 15 21:24:15 2011 +0100
@@ -17,7 +17,7 @@
   val ensure_propT: theory -> term -> term
   val dest_judgment: cterm -> cterm
   val judgment_conv: conv -> conv
-  val is_elim: thm -> bool
+  val elim_concl: thm -> term option
   val declare_atomize: attribute
   val declare_rulify: attribute
   val atomize_term: theory -> term -> term
@@ -145,13 +145,15 @@
 
 (* elimination rules *)
 
-fun is_elim rule =
+fun elim_concl rule =
   let
     val thy = Thm.theory_of_thm rule;
     val concl = Thm.concl_of rule;
+    val C = drop_judgment thy concl;
   in
-    Term.is_Var (drop_judgment thy concl) andalso
+    if Term.is_Var C andalso
       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
+    then SOME C else NONE
   end;