1.1 --- a/src/HOL/Code_Eval.thy	Thu May 14 08:22:06 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Thu May 14 08:22:07 2009 +0200
     1.3 @@ -72,9 +72,7 @@
     1.4          map Free (Name.names Name.context "a" tys));
     1.5        val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
     1.6          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
     1.7 -        handle TYPE (msg, tys, ts) => (tracing msg; error "")
     1.8        val cty = Thm.ctyp_of thy ty;
     1.9 -      val _ = tracing (cat_lines [makestring arg, makestring rhs, makestring cty])
    1.10      in
    1.11        @{thm term_of_anything}
    1.12        |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]