src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -223,8 +223,8 @@
   let
     val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     fun fix (x, T) = (Binding.name (Variable.revert_fixed 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');
+    val xs = map (fix o #2) ps;
+    val As = Logic.strip_imp_prems prop';
   in ((Binding.empty, (xs, As)), ctxt') end;
 
 in
@@ -232,7 +232,6 @@
 fun pretty_statement ctxt kind raw_th =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
@@ -250,7 +249,7 @@
     pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
      (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
       else
-        let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
+        let val (clauses, ctxt'') = fold_map obtain cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
   end |> thm_name kind raw_th;