# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID 88c9c3460fe71a56a710e4829dcdd51c87f50574
# Parent  2eb7dfcf3bc33895b240c9d5ae3679462a097f7e
renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler

diff -r 2eb7dfcf3bc3 -r 88c9c3460fe7 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -141,7 +141,7 @@
 
   inductify : bool,
   rpred : bool,
-  sizelim : bool
+  depth_limited : bool
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
@@ -152,7 +152,7 @@
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
-fun is_sizelim (Options opt) = #sizelim opt
+fun is_depth_limited (Options opt) = #depth_limited opt
 
 val default_options = Options {
   expected_modes = NONE,
@@ -162,7 +162,7 @@
   show_mode_inference = false,
   inductify = false,
   rpred = false,
-  sizelim = false
+  depth_limited = false
 }
 
 
diff -r 2eb7dfcf3bc3 -r 88c9c3460fe7 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -65,9 +65,9 @@
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
       |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
       |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]
-      |> Predicate_Compile_Core.add_sizelim_equations Predicate_Compile_Aux.default_options [full_constname]
+      |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]
       |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname]
-    val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
+    val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
     val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
     val prog =
       if member (op =) modes ([], []) then
@@ -75,9 +75,9 @@
           val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
           val T = @{typ code_numeral} --> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
         in Const (name, T) $ Bound 0 end
-      else if member (op =) sizelim_modes ([], []) then
+      else if member (op =) depth_limited_modes ([], []) then
         let
-          val name = Predicate_Compile_Core.sizelim_function_name_of thy'' full_constname ([], [])
+          val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
           val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
         in lift_pred (Const (name, T) $ Bound 0) end
       else error "Predicate Compile Quickcheck failed"
diff -r 2eb7dfcf3bc3 -r 88c9c3460fe7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -113,7 +113,7 @@
       show_mode_inference = chk "show_mode_inference",
       inductify = chk "inductify",
       rpred = chk "rpred",
-      sizelim = chk "sizelim"
+      depth_limited = chk "depth_limited"
     }
   end
 
@@ -141,7 +141,7 @@
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
-  "show_mode_inference", "inductify", "rpred", "sizelim"]
+  "show_mode_inference", "inductify", "rpred", "depth_limited"]
 
 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)
 
diff -r 2eb7dfcf3bc3 -r 88c9c3460fe7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -23,8 +23,8 @@
   val predfun_name_of: theory -> string -> mode -> string
   val all_preds_of : theory -> string list
   val modes_of: theory -> string -> mode list
-  val sizelim_modes_of: theory -> string -> mode list
-  val sizelim_function_name_of : theory -> string -> mode -> string
+  val depth_limited_modes_of: theory -> string -> mode list
+  val depth_limited_function_name_of : theory -> string -> mode -> string
   val generator_modes_of: theory -> string -> mode list
   val generator_name_of : theory -> string -> mode -> string
   val string_of_mode : mode -> string
@@ -91,7 +91,7 @@
   val dest_funT : typ -> typ * typ
  (* val depending_preds_of : theory -> thm list -> string list *)
   val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
-  val add_sizelim_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val is_inductive_predicate : theory -> string -> bool
   val terms_vs : term list -> string list
   val subsets : int -> int -> int list list
@@ -289,15 +289,15 @@
   nparams : int,
   functions : (mode * predfun_data) list,
   generators : (mode * function_data) list,
-  sizelim_functions : (mode * function_data) list 
+  depth_limited_functions : (mode * function_data) list 
 };
 
 fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim, nparams), (functions, generators, sizelim_functions)) =
+fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =
   PredData {intros = intros, elim = elim, nparams = nparams,
-    functions = functions, generators = generators, sizelim_functions = sizelim_functions}
-fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, sizelim_functions}) =
-  mk_pred_data (f ((intros, elim, nparams), (functions, generators, sizelim_functions)))
+    functions = functions, generators = generators, depth_limited_functions = depth_limited_functions}
+fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) =
+  mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions)))
   
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -342,7 +342,7 @@
 
 val modes_of = (map fst) o #functions oo the_pred_data
 
-val sizelim_modes_of = (map fst) o #sizelim_functions oo the_pred_data
+val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data
 
 val rpred_modes_of = (map fst) o #generators oo the_pred_data
   
@@ -381,16 +381,16 @@
 fun all_generator_modes_of thy =
   map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 
 
-fun lookup_sizelim_function_data thy name mode =
+fun lookup_depth_limited_function_data thy name mode =
   Option.map rep_function_data (AList.lookup (op =)
-  (#sizelim_functions (the_pred_data thy name)) mode)
+  (#depth_limited_functions (the_pred_data thy name)) mode)
 
-fun the_sizelim_function_data thy name mode = case lookup_sizelim_function_data thy name mode
-  of NONE => error ("No size-limited function defined for mode " ^ string_of_mode mode
+fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode
+  of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
     ^ " of predicate " ^ name)
    | SOME data => data
 
-val sizelim_function_name_of = #name ooo the_sizelim_function_data
+val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
 
 (*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
      
@@ -761,7 +761,7 @@
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
-fun set_sizelim_function_name pred mode name = 
+fun set_depth_limited_function_name pred mode name = 
   let
     val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
   in
@@ -928,20 +928,20 @@
       RPredCompFuns.mk_rpredT T) $ random
   end;
 
-fun sizelim_funT_of compfuns (iss, is) T =
+fun depth_limited_funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
+    val paramTs' = map2 (fn SOME is => depth_limited_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
   in
     (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
   end;  
 
-fun mk_sizelim_fun_of compfuns thy (name, T) mode =
-  Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T)
+fun mk_depth_limited_fun_of compfuns thy (name, T) mode =
+  Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
   
 fun mk_generator_of compfuns thy (name, T) mode = 
-  Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T)
+  Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T)
 
 (* Mode analysis *)
 
@@ -1278,14 +1278,14 @@
     fold_rev lambda vs (f (list_comb (t, vs)))
   end;
 
-fun compile_param size thy compfuns (NONE, t) = t
-  | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
+fun compile_param depth thy compfuns (NONE, t) = t
+  | compile_param depth thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
    let
      val (f, args) = strip_comb (Envir.eta_contract t)
      val (params, args') = chop (length ms) args
-     val params' = map (compile_param size thy compfuns) (ms ~~ params)
-     val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
-     val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
+     val params' = map (compile_param depth thy compfuns) (ms ~~ params)
+     val mk_fun_of = case depth of NONE => mk_fun_of | SOME _ => mk_depth_limited_fun_of
+     val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of
      val f' =
        case f of
          Const (name, T) => mk_fun_of compfuns thy (name, T) (iss, is')
@@ -1295,39 +1295,39 @@
      list_comb (f', params' @ args')
    end
 
-fun compile_expr size thy ((Mode (mode, is, ms)), t) =
+fun compile_expr depth thy ((Mode (mode, is, ms)), t) =
   case strip_comb t of
     (Const (name, T), params) =>
        let
-         val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params)
-         val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
+         val params' = map (compile_param depth thy PredicateCompFuns.compfuns) (ms ~~ params)
+         val mk_fun_of = case depth of NONE => mk_fun_of | SOME _ => mk_depth_limited_fun_of
        in
          list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
        end
   | (Free (name, T), args) =>
        let 
-         val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of 
+         val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of 
        in
          list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args)
        end;
        
-fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) inargs =
+fun compile_gen_expr depth thy compfuns ((Mode (mode, is, ms)), t) inargs =
   case strip_comb t of
     (Const (name, T), params) =>
       let
-        val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params)
+        val params' = map (compile_param depth thy PredicateCompFuns.compfuns) (ms ~~ params)
       in
         list_comb (mk_generator_of compfuns thy (name, T) mode, params' @ inargs)
       end
     | (Free (name, T), params) =>
     lift_pred compfuns
-    (list_comb (Free (name, sizelim_funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs))
+    (list_comb (Free (name, depth_limited_funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs))
       
           
 (** specific rpred functions -- move them to the correct place in this file *)
 
-fun mk_Eval_of size ((x, T), NONE) names = (x, names)
-  | mk_Eval_of size ((x, T), SOME mode) names =
+fun mk_Eval_of depth ((x, T), NONE) names = (x, names)
+  | mk_Eval_of depth ((x, T), SOME mode) names =
 	let
     val Ts = binder_types T
     (*val argnames = Name.variant_list names
@@ -1372,32 +1372,32 @@
 			end
 		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
     val (inargs, outargs) = pairself flat (split_list inoutargs)
-    val size_t = case size of NONE => [] | SOME (polarity, size_t) => [polarity, size_t]
-		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs)
+    val depth_t = case depth of NONE => [] | SOME (polarity, depth_t) => [polarity, depth_t]
+		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ depth_t), mk_tuple outargs)
     val t = fold_rev mk_split_lambda args r
   in
     (t, names)
   end;
 
-fun compile_arg size thy param_vs iss arg = 
+fun compile_arg depth thy param_vs iss arg = 
   let
-    val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
+    val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of
     fun map_params (t as Free (f, T)) =
       if member (op =) param_vs f then
         case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of
           SOME is => let val T' = funT_of PredicateCompFuns.compfuns ([], is) T
-            in fst (mk_Eval_of size ((Free (f, T'), T), SOME is) []) end
+            in fst (mk_Eval_of depth ((Free (f, T'), T), SOME is) []) end
         | NONE => t
       else t
       | map_params t = t
     in map_aterms map_params arg end
   
-fun compile_clause compfuns size thy all_vs param_vs (iss, is) inp (ts, moded_ps) =
+fun compile_clause compfuns depth thy all_vs param_vs (iss, is) inp (ts, moded_ps) =
   let
     fun check_constrt t (names, eqs) =
       if is_constrt thy t then (t, (names, eqs)) else
         let
-          val s = Name.variant names "x";
+          val s = Name.variant names "x"
           val v = Free (s, fastype_of t)
         in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 
@@ -1426,12 +1426,12 @@
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us;
-                   val in_ts = map (compile_arg size thy param_vs iss) in_ts
-                   val args = case size of
+                   val in_ts = map (compile_arg depth thy param_vs iss) in_ts
+                   val args = case depth of
                      NONE => in_ts
-                   | SOME (polarity, size_t) => in_ts @ [polarity, size_t]
+                   | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
                    val u = lift_pred compfuns
-                     (list_comb (compile_expr size thy (mode, t), args))
+                     (list_comb (compile_expr depth thy (mode, t), args))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1439,12 +1439,12 @@
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us
-                   val size' = Option.map (apfst HOLogic.mk_not) size
-                   val args = case size' of
+                   val depth' = Option.map (apfst HOLogic.mk_not) depth
+                   val args = case depth' of
                      NONE => in_ts
-                   | SOME (polarity, size_t) => in_ts @ [polarity, size_t]
+                   | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
                    val u = lift_pred compfuns (mk_not PredicateCompFuns.compfuns
-                     (list_comb (compile_expr size' thy (mode, t), args)))
+                     (list_comb (compile_expr depth' thy (mode, t), args)))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1458,17 +1458,17 @@
              | GeneratorPrem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us;
-                   val args = case size of
+                   val args = case depth of
                      NONE => in_ts
-                     | SOME (polarity, size_t) => in_ts @ [polarity, size_t]
-                   val u = compile_gen_expr size thy compfuns (mode, t) args
+                     | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
+                   val u = compile_gen_expr depth thy compfuns (mode, t) args
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Generator (v, T) =>
                  let
-                 val u = lift_random (HOLogic.mk_random T (snd (the size)))
+                 val u = lift_random (HOLogic.mk_random T (snd (the depth)))
                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
                  in
                    (u, rest)
@@ -1482,11 +1482,11 @@
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
-fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
+fun compile_pred compfuns mk_fun_of depth_limited thy all_vs param_vs s T mode moded_cls =
   let
 	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
     val (Us1, Us2) = split_smodeT (snd mode) Ts2
-    val funT_of = if use_size then sizelim_funT_of else funT_of
+    val funT_of = if depth_limited then depth_limited_funT_of else funT_of
     val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1
   	fun mk_input_term (i, NONE) =
 		    [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
@@ -1502,33 +1502,33 @@
 		val in_ts = maps mk_input_term (snd mode)
     val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
     val [depth_name, polarity_name] = Name.variant_list (all_vs @ param_vs) ["depth", "polarity"]
-    val size = Free (depth_name, @{typ "code_numeral"})
+    val depth = Free (depth_name, @{typ "code_numeral"})
     val polarity = Free (polarity_name, @{typ "bool"})
-    val decr_size =
-      if use_size then
+    val decr_depth =
+      if depth_limited then
         SOME (polarity, Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
-          $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}))
+          $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}))
       else
         NONE
     val cl_ts =
-      map (compile_clause compfuns decr_size
+      map (compile_clause compfuns decr_depth
         thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls;
-    val t = foldr1 (mk_sup compfuns) cl_ts
+    val compilation = foldr1 (mk_sup compfuns) cl_ts
     val T' = mk_predT compfuns (mk_tupleT Us2)
     val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     val full_mode = null Us2
-    val size_t = 
-      if_const $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"})
+    val depth_compilation = 
+      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
       $ (if full_mode then 
           if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $ mk_single compfuns HOLogic.unit
         else
           mk_bot compfuns (dest_predT compfuns T'))
-      $ t
+      $ compilation
     val fun_const = mk_fun_of compfuns thy (s, T) mode
-    val eq = if use_size then
-      (list_comb (fun_const, params @ in_ts @ [polarity, size]), size_t)
+    val eq = if depth_limited then
+      (list_comb (fun_const, params @ in_ts @ [polarity, depth]), depth_compilation)
     else
-      (list_comb (fun_const, params @ in_ts), t)
+      (list_comb (fun_const, params @ in_ts), compilation)
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq eq)
   end;
@@ -1711,16 +1711,16 @@
     fold create_definition modes thy
   end;
 
-fun sizelim_create_definitions preds (name, modes) thy =
+fun create_definitions_of_depth_limited_functions preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
-        val mode_cname = create_constname_of_mode thy "sizelim_" name mode
-        val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T
+        val mode_cname = create_constname_of_mode thy "depth_limited_" name mode
+        val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_sizelim_function_name name mode mode_cname 
+        |> set_depth_limited_function_name name mode mode_cname 
       end;
   in
     fold create_definition modes thy
@@ -1730,7 +1730,7 @@
   let
     val Ts = binder_types T
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
+    val paramTs' = map2 (fn SOME is => depth_limited_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
   in
     (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT RPredCompFuns.compfuns (mk_tupleT outargTs))
   end
@@ -2154,8 +2154,8 @@
   map (fn (pred, modes) =>
     (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
     
-fun compile_preds compfuns mk_fun_of use_size thy all_vs param_vs preds moded_clauses =
-  map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred
+fun compile_preds compfuns mk_fun_of depth_limited thy all_vs param_vs preds moded_clauses =
+  map_preds_modes (fn pred => compile_pred compfuns mk_fun_of depth_limited thy all_vs param_vs pred
       (the (AList.lookup (op =) preds pred))) moded_clauses  
   
 fun prove options thy clauses preds modes moded_clauses compiled_terms =
@@ -2351,13 +2351,13 @@
   are_not_defined = fn thy => forall (null o modes_of thy),
   qname = "equation"}
 
-val add_sizelim_equations = gen_add_equations
+val add_depth_limited_equations = gen_add_equations
   {infer_modes = infer_modes,
-  create_definitions = sizelim_create_definitions,
-  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
+  create_definitions = create_definitions_of_depth_limited_functions,
+  compile_preds = compile_preds PredicateCompFuns.compfuns mk_depth_limited_fun_of true,
   prove = prove_by_skip,
-  are_not_defined = fn thy => forall (null o sizelim_modes_of thy),
-  qname = "sizelim_equation"
+  are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
+  qname = "depth_limited_equation"
   }
 
 val add_quickcheck_equations = gen_add_equations
@@ -2420,9 +2420,9 @@
         goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
           (if is_rpred options then
             (add_equations options [const] #>
-             add_sizelim_equations options [const] #> add_quickcheck_equations options [const])
-           else if is_sizelim options then
-             add_sizelim_equations options [const]
+             add_depth_limited_equations options [const] #> add_quickcheck_equations options [const])
+           else if is_depth_limited options then
+             add_depth_limited_equations options [const]
            else
              add_equations options [const]))
       end