--- a/Nominal/Nominal2.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Nominal2.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -569,7 +569,7 @@
   (* FIXME: local version *)
   (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
 
-  val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
+  val thy' = Sign.add_consts constr_trms (Proof_Context.theory_of spec_ctxt)
 in
   (dts', thy')
 end
@@ -591,7 +591,7 @@
 
 in
   (Local_Theory.exit_global lthy')
-  |> Sign.add_consts_i bn_funs'
+  |> Sign.add_consts bn_funs'
   |> pair (bn_funs', bn_eqs) 
 end 
 *}