--- a/src/HOL/Import/proof_kernel.ML Mon Sep 12 16:20:18 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Sep 12 17:29:07 2005 +0200
@@ -121,6 +121,8 @@
type ('a,'b) subst = ('a * 'b) list
datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
+fun hthm2thm (HOLThm (_, th)) = th
+
datatype proof_info
= Info of {disk_info: (string * string) option ref}
@@ -1096,14 +1098,7 @@
fun disamb_terms_from info tms = (info, tms)
-fun disamb_thms_from info hthms =
- foldr (fn (hthm,(info,thms)) =>
- let
- val (info',tm') = disamb_thm_from info hthm
- in
- (info',tm'::thms)
- end)
- (info,[]) hthms
+fun disamb_thms_from info hthms = (info, map hthm2thm hthms)
fun disamb_term tm = disamb_term_from disamb_info_empty tm
fun disamb_terms tms = disamb_terms_from disamb_info_empty tms