# HG changeset patch
# User wenzelm
# Date 1003857300 -7200
# Node ID a71713885e3e5715d3b988476b86defcb5e105ea
# Parent  77c63f8e9d9aedf6fc06a084fa581dbbb286d632
removed export_thm;

diff -r 77c63f8e9d9a -r a71713885e3e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 23 19:14:47 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 23 19:15:00 2001 +0200
@@ -50,7 +50,6 @@
   val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
   val refine: (context -> method) -> state -> state Seq.seq
   val refine_end: (context -> method) -> state -> state Seq.seq
-  val export_thm: context -> thm -> thm
   val match_bind: (string list * string) list -> state -> state
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
@@ -430,14 +429,6 @@
       in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
   in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
 
-fun export_thm inner thm =
-  let val exp_tac = ProofContext.export_wrt false inner None in
-    (case Seq.chop (2, exp_tac thm) of
-      ([thm'], _) => thm'
-    | ([], _) => raise THM ("export: failed", 0, [thm])
-    | _ => raise THM ("export: more than one result", 0, [thm]))
-  end;
-
 fun transfer_facts inner_state state =
   (case get_facts inner_state of
     None => Seq.single (reset_facts state)