tuned
authorhaftmann
Sat Sep 15 19:27:40 2007 +0200 (2007-09-15)
changeset 24585c359896d0f48
parent 24584 01e83ffa6c54
child 24586 c87238132dc3
tuned
doc-src/TutorialI/Misc/appendix.thy
src/HOL/ex/Fundefs.thy
src/Pure/Isar/code.ML
src/Pure/codegen.ML
src/Tools/code/code_package.ML
     1.1 --- a/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:35 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/appendix.thy	Sat Sep 15 19:27:40 2007 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*<*)
     1.5 -theory appendix imports Main begin;
     1.6 +theory appendix
     1.7 +imports Main
     1.8 +begin
     1.9  (*>*)
    1.10  
    1.11  text{*
    1.12 @@ -22,12 +24,10 @@
    1.13  @{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
    1.14  @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.15  @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    1.16 -@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.17 -@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
    1.18 -@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.19 -@{text LEAST}$~x.~P$
    1.20 +%@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
    1.21 +%@{text LEAST}$~x.~P$
    1.22  \end{tabular}
    1.23 -\caption{Overloaded Constants in HOL}
    1.24 +\caption{Algebraic symbols and operations in HOL}
    1.25  \label{tab:overloading}
    1.26  \end{center}
    1.27  \end{table}
     2.1 --- a/src/HOL/ex/Fundefs.thy	Sat Sep 15 19:27:35 2007 +0200
     2.2 +++ b/src/HOL/ex/Fundefs.thy	Sat Sep 15 19:27:40 2007 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4  
     2.5  (* Prove a lemma before attempting a termination proof *)
     2.6  lemma f91_estimate: 
     2.7 -  assumes trm: "f91_dom n" 
     2.8 +  assumes trm: "f91_dom n"
     2.9    shows "n < f91 n + 11"
    2.10  using trm by induct auto
    2.11  
    2.12 @@ -80,7 +80,7 @@
    2.13    show "wf ?R" ..
    2.14  
    2.15    fix n::nat assume "~ 100 < n" (* Inner call *)
    2.16 -  thus "(n + 11, n) : ?R" by simp 
    2.17 +  thus "(n + 11, n) : ?R" by simp
    2.18  
    2.19    assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
    2.20    with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
    2.21 @@ -89,6 +89,7 @@
    2.22  
    2.23  
    2.24  
    2.25 +
    2.26  subsection {* More general patterns *}
    2.27  
    2.28  subsubsection {* Overlapping patterns *}
     3.1 --- a/src/Pure/Isar/code.ML	Sat Sep 15 19:27:35 2007 +0200
     3.2 +++ b/src/Pure/Isar/code.ML	Sat Sep 15 19:27:40 2007 +0200
     3.3 @@ -679,9 +679,9 @@
     3.4            then error ("Rejected equation for datatype constructor:\n"
     3.5              ^ string_of_thm func)
     3.6            else ();
     3.7 -      in map_exec_purge (SOME [c]) (map_funcs
     3.8 -        (Symtab.map_default
     3.9 -          (c, (Susp.value [], [])) (add_thm func))) thy
    3.10 +      in
    3.11 +        (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
    3.12 +          (c, (Susp.value [], [])) (add_thm func)) thy
    3.13        end
    3.14    | add_func false thm thy =
    3.15        case mk_func_liberal thm
     4.1 --- a/src/Pure/codegen.ML	Sat Sep 15 19:27:35 2007 +0200
     4.2 +++ b/src/Pure/codegen.ML	Sat Sep 15 19:27:40 2007 +0200
     4.3 @@ -1031,9 +1031,9 @@
     4.4      val t = eval_term thy (Syntax.read_term ctxt s);
     4.5      val T = Term.type_of t;
     4.6    in
     4.7 -    writeln (Pretty.string_of
     4.8 +    Pretty.writeln
     4.9        (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
    4.10 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
    4.11 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
    4.12    end);
    4.13  
    4.14  exception Evaluation of term;
     5.1 --- a/src/Tools/code/code_package.ML	Sat Sep 15 19:27:35 2007 +0200
     5.2 +++ b/src/Tools/code/code_package.ML	Sat Sep 15 19:27:40 2007 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4      -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
     5.5         -> string list -> cterm -> 'a)
     5.6      -> cterm -> 'a;
     5.7 -  val satisfies_ref: bool option ref;
     5.8 +  val satisfies_ref: (unit -> bool) option ref;
     5.9    val satisfies: theory -> cterm -> string list -> bool;
    5.10    val codegen_command: theory -> string -> unit;
    5.11  
    5.12 @@ -28,8 +28,6 @@
    5.13    val appgen_case: (theory -> term
    5.14      -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
    5.15      -> appgen;
    5.16 -
    5.17 -  val timing: bool ref;
    5.18  end;
    5.19  
    5.20  structure CodePackage : CODE_PACKAGE =
    5.21 @@ -146,22 +144,18 @@
    5.22          ensure_def thy defgen_datatype ("generating type constructor " ^ quote tyco) tyco'
    5.23          #> pair tyco'
    5.24        end
    5.25 -and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) trns =
    5.26 -  trns
    5.27 -  |> fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
    5.28 -  |>> (fn sort => (unprefix "'" v, sort))
    5.29 -and exprgen_typ thy algbr funcgr (TFree vs) trns =
    5.30 -      trns
    5.31 -      |> exprgen_tyvar_sort thy algbr funcgr vs
    5.32 -      |>> (fn (v, sort) => ITyVar v)
    5.33 -  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
    5.34 -      trns
    5.35 -      |> ensure_def_tyco thy algbr funcgr tyco
    5.36 -      ||>> fold_map (exprgen_typ thy algbr funcgr) tys
    5.37 -      |>> (fn (tyco, tys) => tyco `%% tys);
    5.38 +and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
    5.39 +  fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
    5.40 +  #>> (fn sort => (unprefix "'" v, sort))
    5.41 +and exprgen_typ thy algbr funcgr (TFree vs) =
    5.42 +      exprgen_tyvar_sort thy algbr funcgr vs
    5.43 +      #>> (fn (v, sort) => ITyVar v)
    5.44 +  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
    5.45 +      ensure_def_tyco thy algbr funcgr tyco
    5.46 +      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
    5.47 +      #>> (fn (tyco, tys) => tyco `%% tys);
    5.48  
    5.49  exception CONSTRAIN of (string * typ) * typ;
    5.50 -val timing = ref false;
    5.51  
    5.52  fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
    5.53    let
    5.54 @@ -201,118 +195,119 @@
    5.55    in
    5.56      fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
    5.57    end
    5.58 -and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) trns =
    5.59 +and exprgen_eq thy algbr funcgr thm =
    5.60 +  let
    5.61 +    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
    5.62 +      o Logic.unvarify o prop_of) thm;
    5.63 +  in
    5.64 +    fold_map (exprgen_term thy algbr funcgr) args
    5.65 +    ##>> exprgen_term thy algbr funcgr rhs
    5.66 +    #>> rpair thm
    5.67 +  end
    5.68 +and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
    5.69    let
    5.70      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    5.71      val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
    5.72 -    val vs = Name.names (Name.declare var Name.context) "'a" (Sorts.mg_domain algebra tyco [class]);
    5.73 +    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    5.74 +    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    5.75 +    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
    5.76 +      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
    5.77      val arity_typ = Type (tyco, map TFree vs);
    5.78 -    fun gen_superarity superclass trns =
    5.79 -      trns
    5.80 -      |> ensure_def_class thy algbr funcgr superclass
    5.81 -      ||>> ensure_def_classrel thy algbr funcgr (class, superclass)
    5.82 -      ||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
    5.83 -      |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
    5.84 +    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
    5.85 +    fun gen_superarity superclass =
    5.86 +      ensure_def_class thy algbr funcgr superclass
    5.87 +      ##>> ensure_def_classrel thy algbr funcgr (class, superclass)
    5.88 +      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
    5.89 +      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
    5.90              (superclass, (classrel, (inst, dss))));
    5.91 -    fun gen_classop_def (c, ty) trns =
    5.92 -      trns
    5.93 -      |> ensure_def_const thy algbr funcgr c
    5.94 -      ||>> exprgen_term thy algbr funcgr
    5.95 -            (Const (Class.inst_const thy (c, tyco), map_type_tfree (K arity_typ) ty));
    5.96 -    fun defgen_inst trns =
    5.97 -      trns
    5.98 -      |> ensure_def_class thy algbr funcgr class
    5.99 -      ||>> ensure_def_tyco thy algbr funcgr tyco
   5.100 -      ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   5.101 -      ||>> fold_map gen_superarity superclasses
   5.102 -      ||>> fold_map gen_classop_def classops
   5.103 -      |>> (fn ((((class, tyco), arity), superarities), classops) =>
   5.104 +    fun gen_classop_def (c, ty) =
   5.105 +      let
   5.106 +        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   5.107 +        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
   5.108 +        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   5.109 +          o Logic.dest_equals o Thm.prop_of) thm;
   5.110 +      in
   5.111 +        ensure_def_const thy algbr funcgr c
   5.112 +        ##>> exprgen_const thy algbr funcgr c_ty
   5.113 +        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
   5.114 +      end;
   5.115 +    val defgen_inst =
   5.116 +      ensure_def_class thy algbr funcgr class
   5.117 +      ##>> ensure_def_tyco thy algbr funcgr tyco
   5.118 +      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   5.119 +      ##>> fold_map gen_superarity superclasses
   5.120 +      ##>> fold_map gen_classop_def classops
   5.121 +      #>> (fn ((((class, tyco), arity), superarities), classops) =>
   5.122               CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classops)));
   5.123      val inst = CodeName.instance thy (class, tyco);
   5.124    in
   5.125 -    trns
   5.126 -    |> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
   5.127 -    |> pair inst
   5.128 +    ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
   5.129 +    #> pair inst
   5.130    end
   5.131  and ensure_def_const thy (algbr as (_, consts)) funcgr c =
   5.132    let
   5.133      val c' = CodeName.const thy c;
   5.134 -    fun defgen_datatypecons trns =
   5.135 -      trns 
   5.136 -      |> ensure_def_tyco thy algbr funcgr
   5.137 -          ((the o Code.get_datatype_of_constr thy) c)
   5.138 -      |>> (fn _ => CodeThingol.Bot);
   5.139 -    fun defgen_classop trns =
   5.140 -      trns 
   5.141 -      |> ensure_def_class thy algbr funcgr
   5.142 -        ((the o AxClass.class_of_param thy) c)
   5.143 -      |>> (fn _ => CodeThingol.Bot);
   5.144 +    fun defgen_datatypecons tyco =
   5.145 +      ensure_def_tyco thy algbr funcgr tyco
   5.146 +      #>> K CodeThingol.Bot;
   5.147 +    fun defgen_classop class =
   5.148 +      ensure_def_class thy algbr funcgr class
   5.149 +      #>> K CodeThingol.Bot;
   5.150      fun defgen_fun trns =
   5.151        let
   5.152          val raw_thms = CodeFuncgr.funcs funcgr c;
   5.153          val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
   5.154 +        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
   5.155          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   5.156            then raw_thms
   5.157            else map (CodeUnit.expand_eta 1) raw_thms;
   5.158 -        val timeap = if !timing then Output.timeap_msg ("time for " ^ c)
   5.159 -          else I;
   5.160 -        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
   5.161 -        val dest_eqthm =
   5.162 -          apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   5.163 -        fun exprgen_eq (args, rhs) =
   5.164 -          fold_map (exprgen_term thy algbr funcgr) args
   5.165 -          ##>> exprgen_term thy algbr funcgr rhs;
   5.166        in
   5.167          trns
   5.168          |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   5.169          ||>> exprgen_typ thy algbr funcgr ty
   5.170 -        ||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
   5.171 +        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
   5.172          |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
   5.173        end;
   5.174 -    val defgen = if (is_some o Code.get_datatype_of_constr thy) c
   5.175 -      then defgen_datatypecons
   5.176 -      else if (is_some o AxClass.class_of_param thy) c
   5.177 -      then defgen_classop
   5.178 -      else defgen_fun
   5.179 +    val defgen = case Code.get_datatype_of_constr thy c
   5.180 +     of SOME tyco => defgen_datatypecons tyco
   5.181 +      | NONE => (case AxClass.class_of_param thy c
   5.182 +         of SOME class => defgen_classop class
   5.183 +          | NONE => defgen_fun)
   5.184    in
   5.185      ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
   5.186      #> pair c'
   5.187    end
   5.188 -and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
   5.189 -      trns
   5.190 -      |> select_appgen thy algbr funcgr ((c, ty), [])
   5.191 -  | exprgen_term thy algbr funcgr (Free (v, ty)) trns =
   5.192 -      trns
   5.193 -      |> exprgen_typ thy algbr funcgr ty
   5.194 -      |>> (fn _ => IVar v)
   5.195 -  | exprgen_term thy algbr funcgr (Abs (raw_v, ty, raw_t)) trns =
   5.196 +and exprgen_term thy algbr funcgr (Const (c, ty)) =
   5.197 +      select_appgen thy algbr funcgr ((c, ty), [])
   5.198 +  | exprgen_term thy algbr funcgr (Free (v, _)) =
   5.199 +      pair (IVar v)
   5.200 +  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
   5.201        let
   5.202 -        val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
   5.203 +        val (v, t) = Syntax.variant_abs abs;
   5.204        in
   5.205 -        trns
   5.206 -        |> exprgen_typ thy algbr funcgr ty
   5.207 -        ||>> exprgen_term thy algbr funcgr t
   5.208 -        |>> (fn (ty, t) => (v, ty) `|-> t)
   5.209 +        exprgen_typ thy algbr funcgr ty
   5.210 +        ##>> exprgen_term thy algbr funcgr t
   5.211 +        #>> (fn (ty, t) => (v, ty) `|-> t)
   5.212        end
   5.213 -  | exprgen_term thy algbr funcgr (t as _ $ _) trns =
   5.214 +  | exprgen_term thy algbr funcgr (t as _ $ _) =
   5.215        case strip_comb t
   5.216         of (Const (c, ty), ts) =>
   5.217 -            trns
   5.218 -            |> select_appgen thy algbr funcgr ((c, ty), ts)
   5.219 +            select_appgen thy algbr funcgr ((c, ty), ts)
   5.220          | (t', ts) =>
   5.221 -            trns
   5.222 -            |> exprgen_term thy algbr funcgr t'
   5.223 -            ||>> fold_map (exprgen_term thy algbr funcgr) ts
   5.224 -            |>> (fn (t, ts) => t `$$ ts)
   5.225 -and appgen_default thy algbr funcgr ((c, ty), ts) trns =
   5.226 -  trns
   5.227 -  |> ensure_def_const thy algbr funcgr c
   5.228 -  ||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
   5.229 -  ||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
   5.230 -  ||>> exprgen_dict_parms thy algbr funcgr (c, ty)
   5.231 -  ||>> fold_map (exprgen_term thy algbr funcgr) ts
   5.232 -  |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
   5.233 -and select_appgen thy algbr funcgr ((c, ty), ts) trns =
   5.234 +            exprgen_term thy algbr funcgr t'
   5.235 +            ##>> fold_map (exprgen_term thy algbr funcgr) ts
   5.236 +            #>> (fn (t, ts) => t `$$ ts)
   5.237 +and exprgen_const thy algbr funcgr (c, ty) =
   5.238 +  ensure_def_const thy algbr funcgr c
   5.239 +  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
   5.240 +  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
   5.241 +  (*##>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)*)
   5.242 +  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   5.243 +and exprgen_app_default thy algbr funcgr (c_ty, ts) =
   5.244 +  exprgen_const thy algbr funcgr c_ty
   5.245 +  ##>> fold_map (exprgen_term thy algbr funcgr) ts
   5.246 +  #>> (fn (t, ts) => t `$$ ts)
   5.247 +and select_appgen thy algbr funcgr ((c, ty), ts) =
   5.248    case Symtab.lookup (Appgens.get thy) c
   5.249     of SOME (i, (appgen, _)) =>
   5.250          if length ts < i then
   5.251 @@ -323,22 +318,18 @@
   5.252                (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   5.253              val vs = Name.names ctxt "a" tys;
   5.254            in
   5.255 -            trns
   5.256 -            |> fold_map (exprgen_typ thy algbr funcgr) tys
   5.257 -            ||>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
   5.258 -            |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   5.259 +            fold_map (exprgen_typ thy algbr funcgr) tys
   5.260 +            ##>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
   5.261 +            #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   5.262            end
   5.263          else if length ts > i then
   5.264 -          trns
   5.265 -          |> appgen thy algbr funcgr ((c, ty), Library.take (i, ts))
   5.266 -          ||>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   5.267 -          |>> (fn (t, ts) => t `$$ ts)
   5.268 +          appgen thy algbr funcgr ((c, ty), Library.take (i, ts))
   5.269 +          ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   5.270 +          #>> (fn (t, ts) => t `$$ ts)
   5.271          else
   5.272 -          trns
   5.273 -          |> appgen thy algbr funcgr ((c, ty), ts)
   5.274 +          appgen thy algbr funcgr ((c, ty), ts)
   5.275      | NONE =>
   5.276 -        trns
   5.277 -        |> appgen_default thy algbr funcgr ((c, ty), ts);
   5.278 +        exprgen_app_default thy algbr funcgr ((c, ty), ts);
   5.279  
   5.280  
   5.281  (* entrance points into translation kernel *)
   5.282 @@ -380,14 +371,14 @@
   5.283      exprgen_term thy algbr funcgr st
   5.284      ##>> exprgen_typ thy algbr funcgr sty
   5.285      ##>> fold_map clause_gen ds
   5.286 -    ##>> appgen_default thy algbr funcgr app
   5.287 +    ##>> exprgen_app_default thy algbr funcgr app
   5.288      #>> (fn (((se, sty), ds), t0) => ICase (((se, sty), ds), t0))
   5.289    end;
   5.290  
   5.291  fun appgen_let thy algbr funcgr (app as (_, [st, ct])) =
   5.292    exprgen_term thy algbr funcgr ct
   5.293    ##>> exprgen_term thy algbr funcgr st
   5.294 -  ##>> appgen_default thy algbr funcgr app
   5.295 +  ##>> exprgen_app_default thy algbr funcgr app
   5.296    #>> (fn (((v, ty) `|-> be, se), t0) =>
   5.297              ICase (CodeThingol.collapse_let (((v, ty), se), be), t0)
   5.298          | (_, t0) => t0);
   5.299 @@ -399,7 +390,7 @@
   5.300    ##>> exprgen_term thy algbr funcgr tt
   5.301    ##>> exprgen_term thy algbr funcgr (Const ("False", Type ("bool", [])))
   5.302    ##>> exprgen_term thy algbr funcgr tf
   5.303 -  ##>> appgen_default thy algbr funcgr app
   5.304 +  ##>> exprgen_app_default thy algbr funcgr app
   5.305    #>> (fn ((((((tb, B), T), tt), F), tf), t0) => ICase (((tb, B), [(T, tt), (F, tf)]), t0));
   5.306  
   5.307  fun add_appconst (c, appgen) thy =
   5.308 @@ -449,10 +440,10 @@
   5.309            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   5.310            ##>> exprgen_typ thy algbr funcgr ty
   5.311            ##>> exprgen_term' thy algbr funcgr t
   5.312 -          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [([], t)]));
   5.313 +          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
   5.314          fun result (dep, code) =
   5.315            let
   5.316 -            val CodeThingol.Fun ((vs, ty), [([], t)]) = Graph.get_node code value_name;
   5.317 +            val CodeThingol.Fun ((vs, ty), [(([], t), _)]) = Graph.get_node code value_name;
   5.318              val deps = Graph.imm_succs code value_name;
   5.319              val code' = Graph.del_nodes [value_name] code;
   5.320              val code'' = CodeThingol.project_code false [] (SOME deps) code';
   5.321 @@ -470,7 +461,7 @@
   5.322  fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
   5.323  fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
   5.324  
   5.325 -val satisfies_ref : bool option ref = ref NONE;
   5.326 +val satisfies_ref : (unit -> bool) option ref = ref NONE;
   5.327  
   5.328  fun satisfies thy ct witnesses =
   5.329    let