--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 16:54:52 2013 +0100
@@ -307,12 +307,6 @@
val prod_case_distrib = @{lemma "(prod_case g x) z = prod_case (% x y. (g x y) z) x" by (simp add: prod_case_beta)}
-(* FIXME: one of many clones *)
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
(* FIXME: another clone *)
fun eq_conv cv1 cv2 ct =
(case Thm.term_of ct of
@@ -337,7 +331,7 @@
ORELSE' rtac
@{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
- (Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
+ (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
fun elim_image_tac ss = etac @{thm imageE}
THEN' REPEAT_DETERM o CHANGED o
@@ -488,7 +482,7 @@
fun mk_thm (fm, t''') = Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac ss' context fm 1)
fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
- val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
+ val post = Conv.fconv_rule (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
val export = singleton (Variable.export ctxt' ctxt)
in
Option.map (export o post o unfold o mk_thm) (rewrite_term t'')