src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/simpdata.ML	Sun Oct 07 21:19:31 2007 +0200
@@ -32,39 +32,39 @@
 
 (*Analyse a rigid formula*)
 val ZF_conn_pairs =
-  [("Ball",     [bspec]),
+  [("Ball",     [@{thm bspec}]),
    ("All",      [spec]),
    ("op -->",   [mp]),
    ("op &",     [conjunct1,conjunct2])];
 
 (*Analyse a:b, where b is rigid*)
 val ZF_mem_pairs =
-  [("Collect",  [CollectD1,CollectD2]),
-   (@{const_name Diff},     [DiffD1,DiffD2]),
-   (@{const_name Int},   [IntD1,IntD2])];
+  [("Collect",  [@{thm CollectD1}, @{thm CollectD2}]),
+   (@{const_name Diff},     [@{thm DiffD1}, @{thm DiffD2}]),
+   (@{const_name Int},   [@{thm IntD1}, @{thm IntD2}])];
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 change_simpset (fn ss =>
   ss setmksimps (map mk_eq o ZF_atomize o gen_all)
-  addcongs [if_weak_cong]);
+  addcongs [@{thm if_weak_cong}]);
 
 local
 
-val unfold_bex_tac = unfold_tac [Bex_def];
+val unfold_bex_tac = unfold_tac [@{thm Bex_def}];
 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-val unfold_ball_tac = unfold_tac [Ball_def];
+val unfold_ball_tac = unfold_tac [@{thm Ball_def}];
 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
 
 in
 
-val defBEX_regroup = Simplifier.simproc (the_context ())
+val defBEX_regroup = Simplifier.simproc @{theory}
   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
 
-val defBALL_regroup = Simplifier.simproc (the_context ())
+val defBALL_regroup = Simplifier.simproc @{theory}
   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
 
 end;
@@ -72,4 +72,5 @@
 Addsimprocs [defBALL_regroup, defBEX_regroup];
 
 
-val ZF_ss = simpset();
+val ZF_ss = @{simpset};
+