--- a/src/HOL/Import/import_package.ML Wed Nov 29 15:44:56 2006 +0100
+++ b/src/HOL/Import/import_package.ML Wed Nov 29 15:44:57 2006 +0100
@@ -38,47 +38,47 @@
else
fn thy =>
fn th =>
- let
+ let
val sg = sign_of_thm th
- val prem = hd (prems_of th)
+ val prem = hd (prems_of th)
val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
- val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg 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 " ^ (string_of_thm thm))
+ val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg 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 " ^ (string_of_thm thm))
val thm = ProofKernel.disambiguate_frees thm
- val _ = message ("Disambiguate: " ^ (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 _ = message ("Disambiguate: " ^ (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 import_meth = Method.simple_args (Args.name -- Args.name)
- (fn arg =>
- fn ctxt =>
- let
- val thy = ProofContext.theory_of ctxt
- in
- Method.SIMPLE_METHOD (import_tac arg thy)
- end)
+ (fn arg =>
+ fn ctxt =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ Method.SIMPLE_METHOD (import_tac arg thy)
+ end)
val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
end