--- a/Nominal/Nominal2.thy	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/Nominal2.thy	Fri May 16 08:38:23 2014 +0100
@@ -178,9 +178,8 @@
   val raw_induct_thms = #inducts (hd dtinfos)
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
-  val raw_size_thms = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names')
-    |> `(fn thms => (length thms) div 2)
-    |> uncurry drop
+  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
+    (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names')))
 
   val raw_result = RawDtInfo 
     {raw_dt_names = raw_full_dt_names',

--- a/Nominal/Nominal2_Base.thy	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri May 16 08:38:23 2014 +0100
@@ -2951,13 +2951,13 @@
 
 
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
-  case term_of ctrm of @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) =>
+  case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
     let  
 
       fun first_is_neg lhs rhs [] = NONE
         | first_is_neg lhs rhs (thm::thms) =
           (case Thm.prop_of thm of
-             _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) =>
+             _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) =>
                (if l = lhs andalso r = rhs then SOME(thm)
                 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym})
                 else first_is_neg lhs rhs thms)  

--- a/Nominal/nominal_atoms.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_atoms.ML	Fri May 16 08:38:23 2014 +0100
@@ -28,7 +28,7 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)
@@ -80,6 +80,6 @@
   Outer_Syntax.command @{command_spec "atom_decl"}
     "declaration of a concrete atom type" 
       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
-        (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
+        (Toplevel.theory o add_atom_decl))
 
 end;

--- a/Nominal/nominal_function.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_function.ML	Fri May 16 08:38:23 2014 +0100
@@ -181,7 +181,8 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
+        val _ = Proof_Display.print_consts do_print 
+          (Position.thread_data ()) lthy (K false) (map fst fixes)
       in
         (info, 
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false} 

--- a/Nominal/nominal_library.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_library.ML	Fri May 16 08:38:23 2014 +0100
@@ -298,8 +298,7 @@
 (* decompses a formula into params, premises and a conclusion *)
 fun strip_full_horn trm =
   let
-    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = 
-      strip_outer_params t |>> cons (a, T)
+    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
     | strip_outer_params B = ([], B)
 
     val (params, body) = strip_outer_params trm
@@ -365,13 +364,13 @@
 
 val natT = @{typ nat}
     
-fun prod_size_const T1 T2 = 
+fun size_prod_const T1 T2 = 
   let
     val T1_fun = T1 --> natT
     val T2_fun = T2 --> natT
     val prodT = HOLogic.mk_prodT (T1, T2)
   in
-    Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT)
+    Const (@{const_name size_prod}, [T1_fun, T2_fun, prodT] ---> natT)
   end
 
 fun snd_const T1 T2 =
@@ -409,7 +408,7 @@
       (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
          Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
     | (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
-         prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
+         size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
     | _ => HOLogic.size_const T
 
   val measure_trm = mk_measure_trm (mk_size_measure) ctxt

--- a/Nominal/nominal_thmdecls.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_thmdecls.ML	Fri May 16 08:38:23 2014 +0100
@@ -112,7 +112,7 @@
          Syntax.string_of_term (Context.proof_of context) (prop_of thm))
   in
     case prop_of thm of
-      Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+      Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
         if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
           c
         else
@@ -256,7 +256,7 @@
 fun eqvt_transform ctxt thm =
   (case prop_of thm of @{const "Trueprop"} $ _ =>
     thm_4_of_1 ctxt thm
-  | @{const "Pure.imp"} $ _ $ _ =>
+  | @{const Pure.imp} $ _ $ _ =>
     thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
   | _ =>
     error msg)
@@ -279,7 +279,7 @@
     in
       (th', thm_4_of_1 ctxt thm)
     end
-  | @{const "Pure.imp"} $ _ $ _ =>
+  | @{const Pure.imp} $ _ $ _ =>
     let
       val th1 = thm_1_of_2 ctxt thm
     in