# HG changeset patch
# User obua
# Date 1126538947 -7200
# Node ID 0a5eebd5ff581687f7bc3317fb95b92d5649a1ef
# Parent  2fc68de9de1f8beb6f6a037db790f966daeb4584
introduced internal function hthm2thm

diff -r 2fc68de9de1f -r 0a5eebd5ff58 src/HOL/Import/proof_kernel.ML
--- 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