--- a/LamEx.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/LamEx.thy	Sun Dec 06 13:41:42 2009 +0100
@@ -80,35 +80,6 @@
 where
   "fv \<equiv> rfv"
 
-ML {*
-local
-   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
-   fun pp_list xs = Pretty.list "[" "]" xs
-   fun pp_str s   = Pretty.str s
-   fun pp_qstr s = Pretty.quote (pp_str s)
-   fun pp_int i   = pp_str (string_of_int i)
-   fun pp_sort S = pp_list (map pp_qstr S)
-   fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
-in
-fun raw_pp_typ (TVar ((a, i), S)) =
-       pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
-   | raw_pp_typ (TFree (a, S)) =
-       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
-   | raw_pp_typ (Type (a, tys)) =
-       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
-end *}
-
-ML {*
-PolyML.addPrettyPrinter
-  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)
-
-*}
-
-typ "name set" 
-typ "name => bool"
-
-ML {* @{typ "name set"} *}
-
 thm fv_def
 
 (* definition of overloaded permutation function *)
@@ -203,7 +174,7 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})