# HG changeset patch
# User wenzelm
# Date 1154610187 -7200
# Node ID a5368278a72c6b11ca00ca6b802169425d55e3da
# Parent  a8761e8568deba7608b9caa2ea53687a062f7404
removed True_implies (cf. True_implies_equals);

diff -r a8761e8568de -r a5368278a72c src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Aug 03 15:03:05 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Aug 03 15:03:07 2006 +0200
@@ -25,8 +25,6 @@
 
 open FundefCommon
 
-val True_implies = thm "True_implies"
-
 
 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
     let 
@@ -112,7 +110,7 @@
 	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
 	  = the (get_fundef_data name thy)
 
-	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
+	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
 
 	val tsimps = map (map remove_domain_condition) psimps
 	val tinduct = map remove_domain_condition simple_pinducts