# HG changeset patch
# User wenzelm
# Date 1184013468 -7200
# Node ID a4e93948f72ac2d81771326f1a6bf088e0a85a2c
# Parent  48816d825078c2214feea081ea9296e11030ccf7
removed legacy ML file;
fixed prems_conv;

diff -r 48816d825078 -r a4e93948f72a src/HOL/Tools/ComputeHOL.ML
--- a/src/HOL/Tools/ComputeHOL.ML	Mon Jul 09 22:06:49 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-signature ComputeHOL =
-sig
-  val prep_thms : thm list -> thm list
-  val to_meta_eq : thm -> thm
-  val to_hol_eq : thm -> thm
-  val symmetric : thm -> thm 
-  val trans : thm -> thm -> thm
-end
-
-structure ComputeHOL : ComputeHOL =
-struct
-
-fun all_prems_conv ci ct = Conv.prems_conv (Logic.count_prems (term_of ct)) ci ct
-
-local
-fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
-in
-fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
-  | rewrite_conv (eq :: eqs) ct =
-      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
-      handle Pattern.MATCH => rewrite_conv eqs ct;
-end
-
-val convert_conditions = Conv.fconv_rule (all_prems_conv (fn _ => Conv.else_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}], Conv.all_conv)))
-
-val eq_th = @{thm "HOL.eq_reflection"}
-val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
-val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
-
-fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
-
-fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
-
-fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
-
-local
-    val sym_HOL = @{thm "HOL.sym"}
-    val sym_Pure = @{thm "ProtoPure.symmetric"}
-in
-  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
-end
-
-local
-    val trans_HOL = @{thm "HOL.trans"}
-    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
-    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
-    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
-    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
-      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
-in
-  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
-end
-
-end
\ No newline at end of file
diff -r 48816d825078 -r a4e93948f72a src/HOL/Tools/ComputeHOL.thy
--- a/src/HOL/Tools/ComputeHOL.thy	Mon Jul 09 22:06:49 2007 +0200
+++ b/src/HOL/Tools/ComputeHOL.thy	Mon Jul 09 22:37:48 2007 +0200
@@ -138,4 +138,59 @@
 
 lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
 
+ML {*
+signature ComputeHOL =
+sig
+  val prep_thms : thm list -> thm list
+  val to_meta_eq : thm -> thm
+  val to_hol_eq : thm -> thm
+  val symmetric : thm -> thm 
+  val trans : thm -> thm -> thm
 end
+
+structure ComputeHOL : ComputeHOL =
+struct
+
+local
+fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
+in
+fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
+  | rewrite_conv (eq :: eqs) ct =
+      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
+      handle Pattern.MATCH => rewrite_conv eqs ct;
+end
+
+val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
+
+val eq_th = @{thm "HOL.eq_reflection"}
+val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
+val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
+
+fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
+
+fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
+
+fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
+
+local
+    val sym_HOL = @{thm "HOL.sym"}
+    val sym_Pure = @{thm "ProtoPure.symmetric"}
+in
+  fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
+end
+
+local
+    val trans_HOL = @{thm "HOL.trans"}
+    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
+    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
+    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
+    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
+      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
+in
+  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
+end
+
+end
+*}
+
+end