--- a/FSet.thy	Sun Nov 22 15:30:23 2009 +0100
+++ b/FSet.thy	Mon Nov 23 10:04:35 2009 +0100
@@ -430,13 +430,11 @@
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 ML {* ObjectLogic.rulify t_s *}
 
-ML {* Type.freeze *}
-
 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
 ML {* val vars = map Free (Term.add_frees gl []) *}
 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
 ML {* val gla = fold lambda_all vars gl *}
-ML {* val glf = Type.freeze gla *}
+ML {* val glf = Type.legacy_freeze gla *}
 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
 
 ML {*
@@ -490,6 +488,16 @@
     | _ => HOLogic.eq_const ty)
 *}
 
+ML mk_babs
+
+ML {*
+fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
+fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
+*}
+
+
 ML {*
 fun my_reg2 lthy trm gtrm =
   case (trm, gtrm) of