# HG changeset patch
# User bulwahn
# Date 1249367696 -7200
# Node ID 89f3c616a2d16fb2ee0fd0de18df6a5724614e5a
# Parent  4a18f3cf63626247bd9884b4c36e2dba587e91fa
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures

diff -r 4a18f3cf6362 -r 89f3c616a2d1 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 04 08:34:56 2009 +0200
@@ -62,7 +62,7 @@
 by auto
 
 (* Setup requires quick and dirty proof *)
-(*
+
 code_pred tranclp
 proof -
   case tranclp
@@ -70,7 +70,7 @@
 qed
 
 thm tranclp.equation
-*)
+
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
diff -r 4a18f3cf6362 -r 89f3c616a2d1 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
@@ -39,17 +39,47 @@
   val mk_Eval : term * term -> term*)
   val mk_tupleT : typ list -> typ
 (*  val mk_predT :  typ -> typ *)
-  (* temporary for compilation *)
-  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term;
+  (* temporary for testing of the compilation *)
+  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
+    GeneratorPrem of term list * term | Generator of (string * typ);
   val prepare_intrs: theory -> string list ->
     (string * typ) list * int * string list * string list * (string * mode list) list *
     (string * (term list * indprem list) list) list * (string * (int option list * int)) list
+  datatype compilation_funs = CompilationFuns of {
+    mk_predT : typ -> typ,
+    dest_predT : typ -> typ,
+    mk_bot : typ -> term,
+    mk_single : term -> term,
+    mk_bind : term * term -> term,
+    mk_sup : term * term -> term,
+    mk_if : term -> term,
+    mk_not : term -> term,
+    funT_of : mode -> typ -> typ,
+    mk_fun_of : theory -> (string * typ) -> mode -> term,
+    lift_pred : term -> term
+  };  
   datatype tmode = Mode of mode * int list * tmode option list;
-  val infer_modes : theory -> (string * (int list option list * int list) list) list
+  type moded_clause = term list * (indprem * tmode) list
+  type 'a pred_mode_table = (string * (mode * 'a) list) list
+  val infer_modes : bool -> theory -> (string * (int list option list * int list) list) list
     -> (string * (int option list * int)) list -> string list
     -> (string * (term list * indprem list) list) list
-    -> (string * (mode * ((term list * (indprem * tmode) list) list)) list) list
+    -> (moded_clause list) pred_mode_table
+  val infer_modes_with_generator : theory -> (string * (int list option list * int list) list) list
+    -> (string * (int option list * int)) list -> string list
+    -> (string * (term list * indprem list) list) list
+    -> (moded_clause list) pred_mode_table  
+  val compile_preds : theory -> compilation_funs -> string list -> string list
+    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table
+  val rpred_create_definitions :(string * typ) list -> int -> string * mode list
+    -> theory -> theory 
   val split_mode : int list -> term list -> (term list * term list)
+  val print_moded_clauses :
+    theory -> (moded_clause list) pred_mode_table -> unit
+  val print_compiled_terms : theory -> term pred_mode_table -> unit
+  val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table
+  val rpred_compfuns : compilation_funs
+  val dest_funT : typ -> typ * typ
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
@@ -100,116 +130,31 @@
   | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
   | dest_tuple t = [t]
 
-(** data structures for generic compilation for different monads **)
-(* maybe rename functions more generic:
-  mk_predT -> mk_monadT; dest_predT -> dest_monadT
-  mk_single -> mk_return (?)
-*)
-datatype compilation_funs = CompilationFuns of {
-  mk_predT : typ -> typ,
-  dest_predT : typ -> typ,
-  mk_bot : typ -> term,
-  mk_single : term -> term,
-  mk_bind : term * term -> term,
-  mk_sup : term * term -> term,
-  mk_if : term -> term,
-  mk_not : term -> term
-};
-
-fun mk_predT (CompilationFuns funs) = #mk_predT funs
-fun dest_predT (CompilationFuns funs) = #dest_predT funs
-fun mk_bot (CompilationFuns funs) = #mk_bot funs
-fun mk_single (CompilationFuns funs) = #mk_single funs
-fun mk_bind (CompilationFuns funs) = #mk_bind funs
-fun mk_sup (CompilationFuns funs) = #mk_sup funs
-fun mk_if (CompilationFuns funs) = #mk_if funs
-fun mk_not (CompilationFuns funs) = #mk_not funs
-  
-structure PredicateCompFuns =
-struct
-
-fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
-
-fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
-  | dest_predT T = raise TYPE ("dest_predT", [T], []);
-
-fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
-
-fun mk_single t =
-  let val T = fastype_of t
-  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
-
-fun mk_bind (x, f) =
-  let val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
+fun mk_scomp (t, u) =
+  let
+    val T = fastype_of t
+    val U = fastype_of u
+    val [A] = binder_types T
+    val D = body_type U 
+  in 
+    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name sup};
-
-fun mk_if cond = Const (@{const_name Predicate.if_pred},
-  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
-
-fun mk_not t = let val T = mk_predT HOLogic.unitT
-  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
-
-fun mk_Enum f =
-  let val T as Type ("fun", [T', _]) = fastype_of f
+fun dest_funT (Type ("fun",[S, T])) = (S, T)
+  | dest_funT T = raise TYPE ("dest_funT", [T], [])
+ 
+fun mk_fun_comp (t, u) =
+  let
+    val (_, B) = dest_funT (fastype_of t)
+    val (C, A) = dest_funT (fastype_of u)
+    val _ = tracing (Syntax.string_of_typ_global @{theory} A)
   in
-    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
+    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
   end;
 
-fun mk_Eval (f, x) =
-  let val T = fastype_of x
-  in
-    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
-  end;
-  
-val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not} 
-
-end;
-
-structure RPredCompFuns =
-struct
-
-fun mk_rpredT T =
-  @{typ "Random.seed"} --> HOLogic.mk_prodT ((PredicateCompFuns.mk_predT T), @{typ "Random.seed"})
-
-fun dest_rpredT (Type ("fun", [_,
-  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
-  | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); 
-
-fun mk_rpredT T =
-  @{typ "Random.seed"} --> HOLogic.mk_prodT ((PredicateCompFuns.mk_predT T), @{typ "Random.seed"})
-
-fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
-
-fun mk_single t =
-  let
-    val T = fastype_of t
-  in
-    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
-  end;
-
-fun mk_bind (x, f) =
-  let
-    val T as (Type ("fun", [_, U])) = fastype_of f
-  in
-    Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
-  end
-
-val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
-
-fun mk_if cond = Const (@{const_name RPred.if_rpred},
-  HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
-
-fun mk_not t = error "Negation is not defined for RPred"
-
-val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not} 
-
-end;
+fun dest_randomT (Type ("fun", [@{typ Random.seed}, T])) =
+  fst (HOLogic.dest_prodT (fst (HOLogic.dest_prodT T)))  
+  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
 (* destruction of intro rules *)
 
@@ -225,6 +170,15 @@
 type mode = int list option list * int list; (*pmode FIMXE*)
 datatype tmode = Mode of mode * int list * tmode option list;
 
+(* short names for nested types *)
+
+datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
+  GeneratorPrem of term list * term | Generator of (string * typ);
+
+type moded_clause = term list * (indprem * tmode) list
+type 'a pred_mode_table = (string * (mode * 'a) list) list
+
+
 fun string_of_mode (iss, is) = space_implode " -> " (map
   (fn NONE => "X"
     | SOME js => enclose "[" "]" (commas (map string_of_int js)))
@@ -245,18 +199,29 @@
 fun mk_predfun_data (name, definition, intro, elim) =
   PredfunData {name = name, definition = definition, intro = intro, elim = elim}
 
+datatype generator_data = GeneratorData of {
+  name : string,
+  equation : thm option
+};
+
+fun rep_generator_data (GeneratorData data) = data;
+fun mk_generator_data (name, equation) =
+  GeneratorData {name = name, equation = equation}
+
 datatype pred_data = PredData of {
   intros : thm list,
   elim : thm option,
   nparams : int,
-  functions : (mode * predfun_data) list
+  functions : (mode * predfun_data) list,
+  generators : (mode * generator_data) list
 };
 
 fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim, nparams), functions) =
-  PredData {intros = intros, elim = elim, nparams = nparams, functions = functions}
-fun map_pred_data f (PredData {intros, elim, nparams, functions}) =
-  mk_pred_data (f ((intros, elim, nparams), functions))
+fun mk_pred_data ((intros, elim, nparams), (functions, generators)) =
+  PredData {intros = intros, elim = elim, nparams = nparams,
+    functions = functions, generators = generators}
+fun map_pred_data f (PredData {intros, elim, nparams, functions, generators}) =
+  mk_pred_data (f ((intros, elim, nparams), (functions, generators)))
   
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -310,8 +275,8 @@
   (#functions (the_pred_data thy name)) mode)
 
 fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
- of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
-  | SOME data => data;
+  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
+   | SOME data => data;
 
 val predfun_name_of = #name ooo the_predfun_data
 
@@ -321,6 +286,18 @@
 
 val predfun_elim_of = #elim ooo the_predfun_data
 
+fun lookup_generator_data thy name mode = 
+  Option.map rep_generator_data (AList.lookup (op =)
+  (#generators (the_pred_data thy name)) mode)
+  
+fun the_generator_data thy name mode = case lookup_generator_data thy name mode
+  of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
+   | SOME data => data
+
+val generator_name_of = #name ooo the_generator_data
+
+(* further functions *)
+
 (* TODO: maybe join chop nparams and split_mode is
 to some function split_mode mode and rename split_mode to split_smode *)
 fun split_mode is ts = let
@@ -329,27 +306,7 @@
         (split_mode' is (i+1) ts)
 in split_mode' is 1 ts end
 
-(* Remark: types of param_funT_of and funT_of are swapped - which is the more
-canonical order? *)
-(* maybe remove param_funT_of completely - by using funT_of *)
-fun param_funT_of compfuns T NONE = T
-  | param_funT_of compfuns T (SOME mode) = let
-     val Ts = binder_types T;
-     val (Us1, Us2) = split_mode mode Ts
-   in Us1 ---> (mk_predT compfuns (mk_tupleT Us2)) end;
-
-fun funT_of compfuns (iss, is) T = let
-    val Ts = binder_types T
-    val (paramTs, argTs) = chop (length iss) Ts
-    val paramTs' = map2 (fn SOME is => funT_of compfuns ([], is) | NONE => I) iss paramTs 
-    val (inargTs, outargTs) = split_mode is argTs
-  in
-    (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
-  end; 
-
-(* TODO: duplicate code in funT_of and this function *)
-fun mk_predfun_of thy compfuns (name, T) mode = 
-  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
+(* diagnostic display functions *)
 
 fun print_stored_rules thy =
   let
@@ -454,8 +411,9 @@
   
 (* updaters *)
 
-fun add_predfun name mode data = let
-    val add = apsnd (cons (mode, mk_predfun_data data))
+fun add_predfun name mode data =
+  let
+    val add = (apsnd o apfst o cons) (mode, mk_predfun_data data)
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate thy name =
@@ -468,7 +426,7 @@
 fun dependencies_of thy name =
   let
     val (intros, elim, nparams) = fetch_pred_data thy name 
-    val data = mk_pred_data ((intros, SOME elim, nparams), [])
+    val data = mk_pred_data ((intros, SOME elim, nparams), ([], []))
     val keys = depending_preds_of thy intros
   in
     (data, keys)
@@ -484,7 +442,7 @@
      | NONE =>
        let
          val nparams = the_default 0 (try (#3 o fetch_pred_data thy) name)
-       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), [])) gr end;
+       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], []))) gr end;
   in PredData.map cons_intro thy end
 
 fun set_elim thm = let
@@ -500,11 +458,199 @@
 fun register_predicate (intros, elim, nparams) thy = let
     val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
   in
-    PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
+    PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [])))
       #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
   end
 
+fun set_generator_name pred mode name = 
+  let
+    val set = (apsnd o apsnd o cons) (mode, mk_generator_data (name, NONE))
+  in
+    PredData.map (Graph.map_node pred (map_pred_data set))
+  end
+
+
+(** data structures for generic compilation for different monads **)
+
+(* maybe rename functions more generic:
+  mk_predT -> mk_monadT; dest_predT -> dest_monadT
+  mk_single -> mk_return (?)
+*)
+datatype compilation_funs = CompilationFuns of {
+  mk_predT : typ -> typ,
+  dest_predT : typ -> typ,
+  mk_bot : typ -> term,
+  mk_single : term -> term,
+  mk_bind : term * term -> term,
+  mk_sup : term * term -> term,
+  mk_if : term -> term,
+  mk_not : term -> term,
+  funT_of : mode -> typ -> typ,
+  mk_fun_of : theory -> (string * typ) -> mode -> term,
+  lift_pred : term -> term
+};
+
+fun mk_predT (CompilationFuns funs) = #mk_predT funs
+fun dest_predT (CompilationFuns funs) = #dest_predT funs
+fun mk_bot (CompilationFuns funs) = #mk_bot funs
+fun mk_single (CompilationFuns funs) = #mk_single funs
+fun mk_bind (CompilationFuns funs) = #mk_bind funs
+fun mk_sup (CompilationFuns funs) = #mk_sup funs
+fun mk_if (CompilationFuns funs) = #mk_if funs
+fun mk_not (CompilationFuns funs) = #mk_not funs
+fun funT_of (CompilationFuns funs) = #funT_of funs
+fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs
+fun lift_pred (CompilationFuns funs) = #lift_pred funs
+
+structure PredicateCompFuns =
+struct
+
+fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
+
+fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
+  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
+
+fun mk_single t =
+  let val T = fastype_of t
+  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+  let val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name sup};
+
+fun mk_if cond = Const (@{const_name Predicate.if_pred},
+  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_not t = let val T = mk_predT HOLogic.unitT
+  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+
+fun mk_Enum f =
+  let val T as Type ("fun", [T', _]) = fastype_of f
+  in
+    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
+  end;
+
+fun mk_Eval (f, x) =
+  let val T = fastype_of x
+  in
+    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
+  end;
+
+fun funT_of (iss, is) T =
+  let
+    val Ts = binder_types T
+    val (paramTs, argTs) = chop (length iss) Ts
+    val paramTs' = map2 (fn SOME is => funT_of ([], is) | NONE => I) iss paramTs 
+    val (inargTs, outargTs) = split_mode is argTs
+  in
+    (paramTs' @ inargTs) ---> (mk_predT (mk_tupleT outargTs))
+  end;  
+
+fun mk_fun_of thy (name, T) mode = 
+  Const (predfun_name_of thy name mode, funT_of mode T)
+
+val lift_pred = I
+
+val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
+  funT_of = funT_of, mk_fun_of = mk_fun_of, lift_pred = lift_pred} 
+
+end;
+
+(* termify_code:
+val termT = Type ("Code_Eval.term", []);
+fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
+*)
+
+fun lift_random random =
+  let
+    val T = dest_randomT (fastype_of random)
+  in
+    mk_scomp (random,
+      mk_fun_comp (HOLogic.pair_const (PredicateCompFuns.mk_predT T) @{typ Random.seed},
+        mk_fun_comp (Const (@{const_name Predicate.single}, T --> (PredicateCompFuns.mk_predT T)),
+          Const (@{const_name "fst"}, HOLogic.mk_prodT (T, @{typ "unit => term"}) --> T)))) 
+  end;
+    
+
+structure RPredCompFuns =
+struct
+
+fun mk_rpredT T =
+  @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"})
+
+fun dest_rpredT (Type ("fun", [_,
+  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
+  | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); 
+
+fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
+
+fun mk_single t =
+  let
+    val T = fastype_of t
+  in
+    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
+  end;
+
+fun mk_bind (x, f) =
+  let
+    val T as (Type ("fun", [_, U])) = fastype_of f
+  in
+    Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
+  end
+
+val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
+
+fun mk_if cond = Const (@{const_name RPred.if_rpred},
+  HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
+
+fun mk_not t = error "Negation is not defined for RPred"
+
+fun funT_of (iss, is) T =
+  let
+    val Ts = binder_types T
+    (* termify code: val Ts = map termifyT Ts *)
+    val (paramTs, argTs) = chop (length iss) Ts
+    val paramTs' = map2 (fn SOME is => funT_of ([], is) | NONE => I) iss paramTs 
+    val (inargTs, outargTs) = split_mode is argTs
+  in
+    (paramTs' @ inargTs) ---> (mk_rpredT (mk_tupleT outargTs))
+  end;
   
+fun mk_fun_of thy (name, T) mode = 
+  Const (generator_name_of thy name mode, funT_of mode T)
+   
+fun lift_pred t =
+  let
+    val T = PredicateCompFuns.dest_predT (fastype_of t)
+    val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T 
+  in
+    Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t  
+  end;
+
+val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
+    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
+    funT_of = funT_of, mk_fun_of = mk_fun_of, lift_pred = lift_pred} 
+
+end;
+(* for external use with interactive mode *)
+val rpred_compfuns = RPredCompFuns.compfuns;
+
+(* Remark: types of param_funT_of and funT_of are swapped - which is the more
+canonical order? *)
+(* maybe remove param_funT_of completely - by using funT_of *)
+fun param_funT_of compfuns T NONE = T
+  | param_funT_of compfuns T (SOME mode) = let
+     val Ts = binder_types T;
+     val (Us1, Us2) = split_mode mode Ts
+   in Us1 ---> (mk_predT compfuns (mk_tupleT Us2)) end;
+
 (* Mode analysis *)
 
 (*** check if a term contains only constructor functions ***)
@@ -553,6 +699,7 @@
 
   
 (*TODO: cleanup function and put together with modes_of_term *)
+(*
 fun modes_of_param default modes t = let
     val (vs, t') = strip_abs t
     val b = length vs
@@ -586,7 +733,9 @@
     | (Free (name, _), args) => the (mk_modes name args)
     | _ => default end
   
-and modes_of_term modes t =
+and
+*)
+fun modes_of_term modes t =
   let
     val ks = 1 upto length (binder_types (fastype_of t));
     val default = [Mode (([], ks), ks, [])];
@@ -618,21 +767,35 @@
     | _ => default
   end
 
-datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term;
-
-fun print_clausess thy clausess =
+fun print_pred_mode_table string_of_entry thy pred_mode_table =
   let
-    val _ = Output.tracing "function print_clauses"
-    fun print_prem (Prem (ts, p)) = Syntax.string_of_term_global thy (list_comb (p, ts)) 
-      | print_prem _ = error "print_clausess: unimplemented"
-    fun print_clause pred (ts, prems) =
-      (space_implode " --> " (map print_prem prems)) ^ " --> " ^ pred ^ " "
-      ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
-    fun print_clauses (pred, clauses) =
-      "clauses of " ^ pred ^ ": " ^ cat_lines (map (print_clause pred) clauses)
-    val _ = Output.tracing (cat_lines (map print_clauses clausess))
+    fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
+      ^ (string_of_entry pred mode entry)  
+    fun print_pred (pred, modes) =
+      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
+    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
+fun print_moded_clauses thy =
+  let
+    fun string_of_moded_prem (Prem (ts, p), Mode (_, is, _)) =
+      (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
+        "(mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
+      | string_of_moded_prem (GeneratorPrem (ts, p), Mode (_, is, _)) =
+      (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
+        "(generator_mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
+      | string_of_moded_prem (Generator (v, T), _) =
+        "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
+      | string_of_moded_prem _ = error "string_of_moded_prem: unimplemented"
+     
+    fun string_of_clause pred mode clauses =
+      cat_lines (map (fn (ts, prems) => (space_implode " --> " (map string_of_moded_prem prems)) ^ " --> " ^ pred ^ " "
+        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
+  in print_pred_mode_table string_of_clause thy end;
+
+fun print_compiled_terms thy =
+  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
+  
 fun select_mode_prem thy modes vs ps =
   find_first (is_some o snd) (ps ~~ map
     (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
@@ -659,15 +822,51 @@
       | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
           else NONE
       ) ps);
-      
-fun check_mode_clause thy param_vs modes (iss, is) (ts, ps) =
+
+fun fold_prem f (Prem (args, _)) = fold f args
+  | fold_prem f (Negprem (args, _)) = fold f args
+  | fold_prem f (Sidecond t) = f t
+
+fun all_subsets [] = [[]]
+  | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end
+
+fun generator vTs v = 
+  let
+    val T = the (AList.lookup (op =) vTs v)
+  in
+    (Generator (v, T), Mode (([], []), [], []))
+  end;
+
+fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t) 
+  | gen_prem _ = error "gen_prem : invalid input for gen_prem"
+  
+fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
   let
     val modes' = modes @ List.mapPartial
       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
-        (param_vs ~~ iss); 
+        (param_vs ~~ iss);
+    val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
+    val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps [])
     fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs)
       | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of
-          NONE => NONE
+          NONE =>
+            (if with_generator then
+              (case select_mode_prem thy gen_modes vs ps of
+                  SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
+                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+                  (filter_out (equal p) ps)
+                | NONE =>
+                  let 
+                    val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
+                  in
+                    case (find_first (fn generator_vs => is_some
+                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
+                      SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
+                        (vs union generator_vs) ps
+                    | NONE => NONE
+                  end)
+            else
+              NONE)
         | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
             (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
             (filter_out (equal p) ps))
@@ -679,43 +878,60 @@
     forall (is_eqT o fastype_of) in_ts' then
       case check_mode_prems [] (param_vs union in_vs) ps of
          NONE => NONE
-       | SOME (acc_ps, vs) => if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+       | SOME (acc_ps, vs) =>
+         if with_generator then
+           SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
+         else
+           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
     else NONE
   end;
 
-fun check_modes_pred thy param_vs preds modes (p, ms) =
+fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
   let val SOME rs = AList.lookup (op =) preds p
   in (p, List.filter (fn m => case find_index
-    (is_none o check_mode_clause thy param_vs modes m) rs of
+    (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
       ~1 => true
     | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
       p ^ " violates mode " ^ string_of_mode m); false)) ms)
   end;
 
-fun get_modes_pred thy param_vs preds modes (p, ms) =
+fun get_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
   let
     val SOME rs = AList.lookup (op =) preds p 
   in
-    (p, map (fn m => (m, map (the o check_mode_clause thy param_vs modes m) rs)) ms)
+    (p, map (fn m => (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
   end;
   
 fun fixp f (x : (string * mode list) list) =
   let val y = f x
   in if x = y then x else fixp f y end;
 
-fun infer_modes thy extra_modes arities param_vs preds =
+fun modes_of_arities arities =
+  (map (fn (s, (ks, k)) => (s, cprod (cprods (map
+            (fn NONE => [NONE]
+              | SOME k' => map SOME (subsets 1 k')) ks),
+            subsets 1 k))) arities)
+  
+fun infer_modes with_generator thy extra_modes arities param_vs preds =
   let
     val modes =
       fixp (fn modes =>
-        map (check_modes_pred thy param_vs preds (modes @ extra_modes)) modes)
-          (map (fn (s, (ks, k)) => (s, cprod (cprods (map
-            (fn NONE => [NONE]
-              | SOME k' => map SOME (subsets 1 k')) ks),
-            subsets 1 k))) arities)
+        map (check_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes)
+          (modes_of_arities arities)
   in
-    map (get_modes_pred thy param_vs preds (modes @ extra_modes)) modes
+    map (get_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes
   end;
-  
+
+fun infer_modes_with_generator thy extra_modes arities param_vs preds =
+  let
+    val modes =
+      fixp (fn modes =>
+        map (check_modes_pred true thy param_vs preds extra_modes modes) modes)
+          (modes_of_arities arities)
+  in
+    map (get_modes_pred true thy param_vs preds extra_modes modes) modes
+  end;
+
 (* term construction *)
 
 fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
@@ -737,7 +953,7 @@
   | distinct_v x nvs = (x, nvs);
 
 fun compile_match thy compfuns eqs eqs' out_ts success_t =
-  let 
+  let
     val eqs'' = maps mk_eq eqs @ eqs'
     val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
     val name = Name.variant names "x";
@@ -802,48 +1018,59 @@
   | compile_param_ext _ _ _ _ = error "compile params"
 *)
 
-fun compile_param thy compfuns modes (NONE, t) = t
- | compile_param thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
-   (* (case t of
-     Abs _ => error "compile_param: Invalid term" *) (* compile_param_ext thy modes (m, t) *)
-   (*  |  _ => let *)
+fun compile_param thy compfuns (NONE, t) = t
+  | compile_param 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 thy compfuns modes) (ms ~~ params)
-     val f' = case f of
-        Const (name, T) =>
-          if AList.defined op = modes name then
-             mk_predfun_of thy compfuns (name, T) (iss, is')
-          else error "compile param: Not an inductive predicate with correct mode"
-      | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is'))
+     val params' = map (compile_param thy compfuns) (ms ~~ params)
+     val f' =
+       case f of
+         Const (name, T) =>
+           mk_fun_of compfuns thy (name, T) (iss, is')
+       | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is'))
    in list_comb (f', params' @ args') end
- | compile_param _ _ _ _ = error "compile params"
-  
-  
-fun compile_expr thy compfuns modes ((Mode (mode, is, ms)), t) =
-      (case strip_comb t of
-         (Const (name, T), params) =>
-           if AList.defined op = modes name then
-             let
-               val params' = map (compile_param thy compfuns modes) (ms ~~ params)
-             in
-               list_comb (mk_predfun_of thy compfuns (name, T) mode, params')
-             end
-           else error "not a valid inductive expression"
-       | (Free (name, T), args) =>
-         (*if name mem param_vs then *)
-         (* Higher order mode call *)
-         let val r = Free (name, param_funT_of compfuns T (SOME is))
-         in list_comb (r, args) end)
-  | compile_expr _ _ _ _ = error "not a valid inductive expression"
+   
+fun compile_expr thy compfuns ((Mode (mode, is, ms)), t) =
+  case strip_comb t of
+    (Const (name, T), params) =>
+       let
+         val params' = map (compile_param thy compfuns) (ms ~~ params)
+       in
+         list_comb (PredicateCompFuns.mk_fun_of thy (name, T) mode, params)
+       end
+  | (Free (name, T), args) =>
+       list_comb (Free (name, param_funT_of compfuns T (SOME is)), args)
+          
+fun compile_gen_expr thy compfuns ((Mode (mode, is, ms)), t) =
+  case strip_comb t of
+    (Const (name, T), params) =>
+       let
+         val params' = map (compile_param thy compfuns) (ms ~~ params)
+       in
+         list_comb (RPredCompFuns.mk_fun_of thy (name, T) mode, params')
+       end
+       
+(** specific rpred functions -- move them to the correct place in this file *)
 
+(* uncommented termify code; causes more trouble than expected at first *) 
+(*
+fun mk_valtermify_term (t as Const (c, T)) = HOLogic.mk_prod (t, Abs ("u", HOLogic.unitT, HOLogic.reflect_term t))
+  | mk_valtermify_term (Free (x, T)) = Free (x, termifyT T) 
+  | mk_valtermify_term (t1 $ t2) =
+    let
+      val T = fastype_of t1
+      val (T1, T2) = dest_funT T
+      val t1' = mk_valtermify_term t1
+      val t2' = mk_valtermify_term t2
+    in
+      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
+    end
+  | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
+*)
 
-fun compile_clause thy compfuns all_vs param_vs modes (iss, is) inp (ts, moded_ps) =
+fun compile_clause thy compfuns all_vs param_vs (iss, is) inp (ts, moded_ps) =
   let
-    val modes' = modes @ List.mapPartial
-      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
-        (param_vs ~~ iss);
     fun check_constrt t (names, eqs) =
       if is_constrt thy t then (t, (names, eqs)) else
         let
@@ -862,6 +1089,10 @@
             val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
               out_ts'' (names', map (rpair []) vs);
           in
+          (* termify code:
+            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
+              (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts)))
+           *)
             compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
               (mk_single compfuns (mk_tuple out_ts))
           end
@@ -876,7 +1107,8 @@
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_mode is us;
-                   val u = list_comb (compile_expr thy compfuns modes (mode, t), in_ts)
+                   val u = lift_pred compfuns
+                     (list_comb (compile_expr thy compfuns (mode, t), in_ts))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -884,7 +1116,8 @@
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_mode is us
-                   val u = list_comb (compile_expr thy compfuns modes (mode, t), in_ts)
+                   val u = lift_pred compfuns
+                     (list_comb (compile_expr thy compfuns (mode, t), in_ts))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (mk_not compfuns u, rest)
@@ -895,6 +1128,21 @@
                  in
                    (mk_if compfuns t, rest)
                  end
+             | GeneratorPrem (us, t) =>
+                 let
+                   val (in_ts, out_ts''') = split_mode is us;
+                   val u = list_comb (compile_gen_expr thy compfuns (mode, t), in_ts)
+                   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 @{term "1::code_numeral"})
+                   val rest = compile_prems [Free (v, T)]  vs' names'' ps;
+                 in
+                   (u, rest)
+                 end
           in
             compile_match thy compfuns constr_vs' eqs out_ts'' 
               (mk_bind compfuns (compiled_clause, rest))
@@ -904,7 +1152,7 @@
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
-fun compile_pred thy compfuns all_vs param_vs modes s T mode moded_cls =
+fun compile_pred thy compfuns all_vs param_vs s T mode moded_cls =
   let
     val Ts = binder_types T;
     val (Ts1, Ts2) = chop (length param_vs) Ts;
@@ -912,33 +1160,18 @@
     val (Us1, _) = split_mode (snd mode) Ts2;
     val xnames = Name.variant_list param_vs
       (map (fn i => "x" ^ string_of_int i) (snd mode));
+    (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *)
     val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
     val cl_ts =
       map (compile_clause thy compfuns
-        all_vs param_vs modes mode (mk_tuple xs)) moded_cls;
+        all_vs param_vs mode (mk_tuple xs)) moded_cls;
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (list_comb (mk_predfun_of thy compfuns (s, T) mode,
+      (list_comb (mk_fun_of compfuns thy (s, T) mode,
          map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs),
        foldr1 (mk_sup compfuns) cl_ts))
   end;
 
-fun map_preds_modes f preds_modes_table =
-  map (fn (pred, modes) =>
-    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table
-
-fun join_preds_modes table1 table2 =
-  map_preds_modes (fn pred => fn mode => fn value =>
-    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
-    
-fun maps_modes preds_modes_table =
-  map (fn (pred, modes) =>
-    (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
-    
-fun compile_preds thy compfuns all_vs param_vs modes preds moded_clauses =
-  map_preds_modes (fn pred => compile_pred thy compfuns all_vs param_vs modes pred
-      (the (AList.lookup (op =) preds pred))) moded_clauses
-
 (* special setup for simpset *)                  
 val HOL_basic_ss' = HOL_basic_ss setSolver 
   (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
@@ -1000,14 +1233,14 @@
   (introthm, elimthm)
 end;
 
-fun create_constname_of_mode thy name mode = 
+fun create_constname_of_mode thy prefix name mode = 
   let
     fun string_of_mode mode = if null mode then "0"
       else space_implode "_" (map string_of_int mode)
     fun string_of_HOmode m s = case m of NONE => s | SOME mode => s ^ "__" ^ (string_of_mode mode)
     val HOmode = fold string_of_HOmode (fst mode) ""
   in
-    (Sign.full_bname thy (Long_Name.base_name name)) ^
+    (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
       (if HOmode = "" then "_" else HOmode ^ "___") ^ (string_of_mode (snd mode))
   end;
   
@@ -1017,7 +1250,7 @@
     val compfuns = PredicateCompFuns.compfuns
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy = let
-      val mode_cname = create_constname_of_mode thy name mode
+      val mode_cname = create_constname_of_mode thy "" name mode
       val mode_cbasename = Long_Name.base_name mode_cname
       val Ts = binder_types T;
       val (Ts1, Ts2) = chop nparams Ts;
@@ -1058,21 +1291,21 @@
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
-        val mode_cname = create_constname_of_mode thy name mode
+        val mode_cname = create_constname_of_mode thy "gen_" name mode
         val Ts = binder_types T;
+        (* termify code: val Ts = map termifyT Ts *)
         val (Ts1, Ts2) = chop nparams Ts;
         val Ts1' = map2 (param_funT_of RPredCompFuns.compfuns) Ts1 (fst mode)
         val (Us1, Us2) = split_mode (snd mode) Ts2;
         val funT = (Ts1' @ Us1) ---> (RPredCompFuns.mk_rpredT (mk_tupleT Us2)) 
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> add_predfun name mode (mode_cname, @{thm refl}, @{thm refl}, @{thm refl}) 
+        |> set_generator_name name mode mode_cname 
       end;
   in
     fold create_definition modes thy
   end;
   
-(**************************************************************************************)
 (* Proving equivalence of term *)
 
 fun is_Type (Type _) = true
@@ -1457,6 +1690,26 @@
        else (fn _ => mycheat_tac thy 1))
   end;
 
+(* composition of mode inference, definition, compilation and proof *)
+
+(** auxillary combinators for table of preds and modes **)
+
+fun map_preds_modes f preds_modes_table =
+  map (fn (pred, modes) =>
+    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table
+
+fun join_preds_modes table1 table2 =
+  map_preds_modes (fn pred => fn mode => fn value =>
+    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
+    
+fun maps_modes preds_modes_table =
+  map (fn (pred, modes) =>
+    (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
+    
+fun compile_preds thy compfuns all_vs param_vs preds moded_clauses =
+  map_preds_modes (fn pred => compile_pred thy compfuns all_vs param_vs pred
+      (the (AList.lookup (op =) preds pred))) moded_clauses  
+  
 fun prove_preds thy clauses preds modes =
   map_preds_modes (prove_pred thy clauses preds modes) 
 
@@ -1471,7 +1724,8 @@
     val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
     val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
     val _ = Output.tracing ("extra_modes are: " ^
-      cat_lines (map (fn (name, modes) => name ^ " has modes:" ^ (commas (map string_of_mode modes))) extra_modes))
+      cat_lines (map (fn (name, modes) => name ^ " has modes:" ^
+      (commas (map string_of_mode modes))) extra_modes))
     val _ $ u = Logic.strip_imp_concl (hd intrs);
     val params = List.take (snd (strip_comb u), nparams);
     val param_vs = maps term_vs params
@@ -1507,27 +1761,28 @@
     val (clauses, arities) = fold add_clause intrs ([], []);
   in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
 
-(* main function *)
+(** main function **)
 
 fun add_equations_of rpred prednames thy =
 let
-  val _ = tracing ("starting add_equations with " ^ commas prednames ^ "...")
+  val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
   val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
     prepare_intrs thy prednames
   val _ = tracing "Infering modes..."
-  val moded_clauses = infer_modes thy extra_modes arities param_vs clauses
+  val moded_clauses = infer_modes false thy extra_modes arities param_vs clauses
   val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
-  val _ = tracing "Defining executable functions..."
+  val _ = Output.tracing "Defining executable functions..."
   val thy' =
     (if rpred then
       fold (rpred_create_definitions preds nparams) modes thy  
     else fold (create_definitions preds nparams) modes thy)
     |> Theory.checkpoint
-  val _ = tracing "Compiling equations..."
+  val _ = Output.tracing "Compiling equations..."
   val compfuns = if rpred then RPredCompFuns.compfuns else PredicateCompFuns.compfuns
   val compiled_terms =
-    compile_preds thy' compfuns all_vs param_vs (extra_modes @ modes) preds moded_clauses
-  val _ = tracing "Proving equations..."
+    compile_preds thy' compfuns all_vs param_vs preds moded_clauses
+  val _ = print_compiled_terms thy' compiled_terms
+  val _ = Output.tracing "Proving equations..."
   val result_thms =
     if rpred then 
       rpred_prove_preds thy' compiled_terms
@@ -1673,7 +1928,7 @@
       | [m] => m
       | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr); m);
-    val t_eval = list_comb (compile_expr thy PredicateCompFuns.compfuns (all_modes_of thy)
+    val t_eval = list_comb (compile_expr thy PredicateCompFuns.compfuns 
       (m, list_comb (pred, params)),
       inargs)
   in t_eval end;