diff -r d1f7b6245a75 -r f5cafe803b55 src/HOL/Import/import.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/import.ML	Fri Jun 19 17:23:21 2009 +0200
@@ -0,0 +1,71 @@
+(*  Title:      HOL/Import/import.ML
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
+signature IMPORT =
+sig
+    val debug      : bool ref
+    val import_tac : Proof.context -> string * string -> tactic
+    val setup      : theory -> theory
+end
+
+structure ImportData = TheoryDataFun
+(
+  type T = ProofKernel.thm option array option
+  val empty = NONE
+  val copy = I
+  val extend = I
+  fun merge _ _ = NONE
+)
+
+structure Import :> IMPORT =
+struct
+
+val debug = ref false
+fun message s = if !debug then writeln s else ()
+
+fun import_tac ctxt (thyname, thmname) =
+    if ! quick_and_dirty
+    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
+    else
+     fn th =>
+        let
+            val thy = ProofContext.theory_of ctxt
+            val prem = hd (prems_of th)
+            val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
+            val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)
+            val int_thms = case ImportData.get thy of
+                               NONE => fst (Replay.setup_int_thms thyname thy)
+                             | SOME a => a
+            val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
+            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
+            val thm = snd (ProofKernel.to_isa_thm hol4thm)
+            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
+            val thm = equal_elim rew thm
+            val prew = ProofKernel.rewrite_hol4_term prem thy
+            val prem' = #2 (Logic.dest_equals (prop_of prew))
+            val _ = message ("Import proved " ^ Display.string_of_thm thm)
+            val thm = ProofKernel.disambiguate_frees thm
+            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
+        in
+            case Shuffler.set_prop thy prem' [("",thm)] of
+                SOME (_,thm) =>
+                let
+                    val _ = if prem' aconv (prop_of thm)
+                            then message "import: Terms match up"
+                            else message "import: Terms DO NOT match up"
+                    val thm' = equal_elim (symmetric prew) thm
+                    val res = bicompose true (false,thm',0) 1 th
+                in
+                    res
+                end
+              | NONE => (message "import: set_prop didn't succeed"; no_tac th)
+        end
+
+val setup = Method.setup @{binding import}
+  (Scan.lift (Args.name -- Args.name) >>
+    (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
+  "import HOL4 theorem"
+
+end
+