diff -r a17b25cb94a6 -r 60ee289a8c63 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu May 13 15:12:34 2010 +0100
+++ b/Nominal/NewParser.thy	Thu May 13 15:58:02 2010 +0100
@@ -185,8 +185,6 @@
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
 *}
 
-ML {* print_depth 50 *}
-
 ML {*
 fun prep_bn lthy dt_names dts eqs = 
 let
@@ -240,7 +238,7 @@
   val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))
   val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
 in
-  ordered' (*map aux2 eqs*)
+  ordered'
 end
 *}
 
@@ -378,15 +376,20 @@
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
 
-val STEPS = 10
+val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10);
+
+fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
 
+setup STEPS_setup
+
+
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatype and raw bn-functions *)
   val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) =
-    if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
@@ -406,7 +409,8 @@
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
+    if get_STEPS lthy > 2 
+    then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
 
   (* definition of raw fv_functions *)
@@ -426,13 +430,15 @@
   val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
    
   val ((fv, fvbn), fv_def, lthy3a) = 
-    if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+    if get_STEPS lthy > 3 
+    then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3
   
 
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
-    if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+    if get_STEPS lthy > 4 
+    then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
     else raise TEST lthy3a
   
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts