explicit distinction between empty code equations and no code equations, including convenient declaration attributes
authorhaftmann
Wed Jan 01 01:05:46 2014 +0100 (2014-01-01)
changeset 548894121d64fde90
parent 54888 6edabf38d929
child 54890 cb892d835803
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
src/Doc/more_antiquote.ML
src/Pure/Isar/code.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:30 2014 +0100
     1.2 +++ b/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:46 2014 +0100
     1.3 @@ -35,6 +35,7 @@
     1.4      val thms = Code_Preproc.cert eqngr const
     1.5        |> Code.equations_of_cert thy
     1.6        |> snd
     1.7 +      |> these
     1.8        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
     1.9        |> map (holize o no_vars ctxt o Axclass.overload thy);
    1.10    in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
     2.1 --- a/src/Pure/Isar/code.ML	Wed Jan 01 01:05:30 2014 +0100
     2.2 +++ b/src/Pure/Isar/code.ML	Wed Jan 01 01:05:46 2014 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4    val conclude_cert: cert -> cert
     2.5    val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
     2.6    val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
     2.7 -    * (((term * string option) list * (term * string option)) * (thm option * bool)) list
     2.8 +    * (((term * string option) list * (term * string option)) * (thm option * bool)) list option
     2.9    val pretty_cert: theory -> cert -> Pretty.T list
    2.10  
    2.11    (*executable code*)
    2.12 @@ -55,6 +55,7 @@
    2.13    val add_nbe_default_eqn_attrib: Attrib.src
    2.14    val del_eqn: thm -> theory -> theory
    2.15    val del_eqns: string -> theory -> theory
    2.16 +  val del_exception: string -> theory -> theory
    2.17    val add_case: thm -> theory -> theory
    2.18    val add_undefined: string -> theory -> theory
    2.19    val get_type: theory -> string
    2.20 @@ -175,6 +176,7 @@
    2.21        (* (cache for default equations, lazy computation of default equations)
    2.22           -- helps to restore natural order of default equations *)
    2.23    | Eqns of (thm * bool) list
    2.24 +  | None
    2.25    | Proj of term * string
    2.26    | Abstr of thm * string;
    2.27  
    2.28 @@ -719,12 +721,13 @@
    2.29  
    2.30  val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
    2.31  
    2.32 -abstype cert = Equations of thm * bool list
    2.33 +abstype cert = Nothing of thm
    2.34 +  | Equations of thm * bool list
    2.35    | Projection of term * string
    2.36    | Abstract of thm * string
    2.37  with
    2.38  
    2.39 -fun empty_cert thy c = 
    2.40 +fun dummy_thm thy c =
    2.41    let
    2.42      val raw_ty = devarify (const_typ thy c);
    2.43      val (vs, _) = typscheme thy (c, raw_ty);
    2.44 @@ -737,9 +740,11 @@
    2.45      val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
    2.46      val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
    2.47      val chead = build_head thy (c, ty);
    2.48 -  in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
    2.49 +  in Thm.weaken chead Drule.dummy_thm end;
    2.50  
    2.51 -fun cert_of_eqns thy c [] = empty_cert thy c
    2.52 +fun nothing_cert thy c = Nothing (dummy_thm thy c);
    2.53 +
    2.54 +fun cert_of_eqns thy c [] = Equations (dummy_thm thy c, [])
    2.55    | cert_of_eqns thy c raw_eqns = 
    2.56        let
    2.57          val eqns = burrow_fst (canonize_thms thy) raw_eqns;
    2.58 @@ -780,38 +785,51 @@
    2.59          ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
    2.60    in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
    2.61  
    2.62 -fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
    2.63 -      let
    2.64 -        val ((vs, _), head) = get_head thy cert_thm;
    2.65 -        val (subst, cert_thm') = cert_thm
    2.66 -          |> Thm.implies_intr head
    2.67 -          |> constrain_thm thy vs sorts;
    2.68 -        val head' = Thm.term_of head
    2.69 -          |> subst
    2.70 -          |> Thm.cterm_of thy;
    2.71 -        val cert_thm'' = cert_thm'
    2.72 -          |> Thm.elim_implies (Thm.assume head');
    2.73 -      in Equations (cert_thm'', propers) end
    2.74 +fun constrain_cert_thm thy sorts cert_thm =
    2.75 +  let
    2.76 +    val ((vs, _), head) = get_head thy cert_thm;
    2.77 +    val (subst, cert_thm') = cert_thm
    2.78 +      |> Thm.implies_intr head
    2.79 +      |> constrain_thm thy vs sorts;
    2.80 +    val head' = Thm.term_of head
    2.81 +      |> subst
    2.82 +      |> Thm.cterm_of thy;
    2.83 +    val cert_thm'' = cert_thm'
    2.84 +      |> Thm.elim_implies (Thm.assume head');
    2.85 +  in cert_thm'' end;
    2.86 +
    2.87 +fun constrain_cert thy sorts (Nothing cert_thm) =
    2.88 +      Nothing (constrain_cert_thm thy sorts cert_thm)
    2.89 +  | constrain_cert thy sorts (Equations (cert_thm, propers)) =
    2.90 +      Equations (constrain_cert_thm thy sorts cert_thm, propers)
    2.91    | constrain_cert thy _ (cert as Projection _) =
    2.92        cert
    2.93    | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
    2.94        Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
    2.95  
    2.96 -fun conclude_cert (Equations (cert_thm, propers)) =
    2.97 -      (Equations (Thm.close_derivation cert_thm, propers))
    2.98 +fun conclude_cert (Nothing cert_thm) =
    2.99 +      Nothing (Thm.close_derivation cert_thm)
   2.100 +  | conclude_cert (Equations (cert_thm, propers)) =
   2.101 +      Equations (Thm.close_derivation cert_thm, propers)
   2.102    | conclude_cert (cert as Projection _) =
   2.103        cert
   2.104    | conclude_cert (Abstract (abs_thm, tyco)) =
   2.105 -      (Abstract (Thm.close_derivation abs_thm, tyco));
   2.106 +      Abstract (Thm.close_derivation abs_thm, tyco);
   2.107  
   2.108 -fun typscheme_of_cert thy (Equations (cert_thm, _)) =
   2.109 +fun typscheme_of_cert thy (Nothing cert_thm) =
   2.110 +      fst (get_head thy cert_thm)
   2.111 +  | typscheme_of_cert thy (Equations (cert_thm, _)) =
   2.112        fst (get_head thy cert_thm)
   2.113    | typscheme_of_cert thy (Projection (proj, _)) =
   2.114        typscheme_projection thy proj
   2.115    | typscheme_of_cert thy (Abstract (abs_thm, _)) =
   2.116        typscheme_abs thy abs_thm;
   2.117  
   2.118 -fun typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
   2.119 +fun typargs_deps_of_cert thy (Nothing cert_thm) =
   2.120 +      let
   2.121 +        val vs = (fst o fst) (get_head thy cert_thm);
   2.122 +      in (vs, []) end
   2.123 +  | typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
   2.124        let
   2.125          val vs = (fst o fst) (get_head thy cert_thm);
   2.126          val equations = if null propers then [] else
   2.127 @@ -826,7 +844,9 @@
   2.128          val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
   2.129        in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end;
   2.130  
   2.131 -fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
   2.132 +fun equations_of_cert thy (cert as Nothing _) =
   2.133 +      (typscheme_of_cert thy cert, NONE)
   2.134 +  | equations_of_cert thy (cert as Equations (cert_thm, propers)) =
   2.135        let
   2.136          val tyscm = typscheme_of_cert thy cert;
   2.137          val thms = if null propers then [] else
   2.138 @@ -835,27 +855,29 @@
   2.139            |> Thm.varifyT_global
   2.140            |> Conjunction.elim_balanced (length propers);
   2.141          fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
   2.142 -      in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   2.143 +      in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end
   2.144    | equations_of_cert thy (Projection (t, tyco)) =
   2.145        let
   2.146          val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
   2.147          val tyscm = typscheme_projection thy t;
   2.148          val t' = Logic.varify_types_global t;
   2.149          fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
   2.150 -      in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end
   2.151 +      in (tyscm, SOME [((abstractions o dest_eqn) t', (NONE, true))]) end
   2.152    | equations_of_cert thy (Abstract (abs_thm, tyco)) =
   2.153        let
   2.154          val tyscm = typscheme_abs thy abs_thm;
   2.155          val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
   2.156          fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
   2.157        in
   2.158 -        (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
   2.159 +        (tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
   2.160            (SOME (Thm.varifyT_global abs_thm), true))])
   2.161        end;
   2.162  
   2.163 -fun pretty_cert thy (cert as Equations _) =
   2.164 +fun pretty_cert thy (cert as Nothing _) =
   2.165 +      [Pretty.str "(not implemented)"]
   2.166 +  | pretty_cert thy (cert as Equations _) =
   2.167        (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
   2.168 -         o snd o equations_of_cert thy) cert
   2.169 +         o these o snd o equations_of_cert thy) cert
   2.170    | pretty_cert thy (Projection (t, _)) =
   2.171        [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
   2.172    | pretty_cert thy (Abstract (abs_thm, _)) =
   2.173 @@ -869,7 +891,7 @@
   2.174  fun retrieve_raw thy c =
   2.175    Symtab.lookup ((the_functions o the_exec) thy) c
   2.176    |> Option.map (snd o fst)
   2.177 -  |> the_default initial_fun_spec
   2.178 +  |> the_default None
   2.179  
   2.180  fun eqn_conv conv ct =
   2.181    let
   2.182 @@ -893,12 +915,12 @@
   2.183  
   2.184  fun get_cert thy { functrans, ss } c =
   2.185    case retrieve_raw thy c
   2.186 -   of Default (_, eqns_lazy) => Lazy.force eqns_lazy
   2.187 +   of Default (eqns, eqns_lazy) => Lazy.force eqns_lazy
   2.188          |> cert_of_eqns_preprocess thy functrans ss c
   2.189      | Eqns eqns => eqns
   2.190          |> cert_of_eqns_preprocess thy functrans ss c
   2.191 -    | Proj (_, tyco) =>
   2.192 -        cert_of_proj thy c tyco
   2.193 +    | None => nothing_cert thy c
   2.194 +    | Proj (_, tyco) => cert_of_proj thy c tyco
   2.195      | Abstr (abs_thm, tyco) => abs_thm
   2.196          |> Thm.transfer thy
   2.197          |> rewrite_eqn thy Conv.arg_conv ss
   2.198 @@ -966,6 +988,7 @@
   2.199      fun pretty_function (const, Default (_, eqns_lazy)) =
   2.200            pretty_equations const (map fst (Lazy.force eqns_lazy))
   2.201        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
   2.202 +      | pretty_function (const, None) = pretty_equations const []
   2.203        | pretty_function (const, Proj (proj, _)) = Pretty.block
   2.204            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
   2.205        | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
   2.206 @@ -1054,6 +1077,7 @@
   2.207        (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
   2.208      fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns))
   2.209            (*this restores the natural order and drops syntactic redundancies*)
   2.210 +      | add_eqn' true None = Default (natural_order [(thm, proper)])
   2.211        | add_eqn' true fun_spec = fun_spec
   2.212        | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
   2.213        | add_eqn' false _ = Eqns [(thm, proper)];
   2.214 @@ -1100,12 +1124,16 @@
   2.215        let
   2.216          fun del_eqn' (Default _) = initial_fun_spec
   2.217            | del_eqn' (Eqns eqns) =
   2.218 -              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
   2.219 +              let
   2.220 +                val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
   2.221 +              in if null eqns' then None else Eqns eqns' end
   2.222            | del_eqn' spec = spec
   2.223        in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   2.224    | NONE => thy;
   2.225  
   2.226 -fun del_eqns c = change_fun_spec c (K initial_fun_spec);
   2.227 +fun del_eqns c = change_fun_spec c (K None);
   2.228 +
   2.229 +fun del_exception c = change_fun_spec c (K (Eqns []));
   2.230  
   2.231  
   2.232  (* cases *)
   2.233 @@ -1229,12 +1257,16 @@
   2.234  val _ = Theory.setup
   2.235    (let
   2.236      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   2.237 +    fun mk_const_attribute f cs =
   2.238 +      mk_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
   2.239      val code_attribute_parser =
   2.240 -      Args.del |-- Scan.succeed (mk_attribute del_eqn)
   2.241 -      || Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_eqn)
   2.242 +      Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_eqn)
   2.243        || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
   2.244        || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
   2.245        || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
   2.246 +      || Args.del |-- Scan.succeed (mk_attribute del_eqn)
   2.247 +      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_eqns)
   2.248 +      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception)
   2.249        || Scan.succeed (mk_attribute add_eqn_maybe_abs);
   2.250    in
   2.251      Datatype_Interpretation.init
     3.1 --- a/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:30 2014 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:46 2014 +0100
     3.3 @@ -369,12 +369,12 @@
     3.4      val names2 = subtract (op =) names_hidden names1;
     3.5      val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
     3.6      val names4 = Graph.all_succs program3 names2;
     3.7 -    val empty_funs = filter_out (member (op =) abortable)
     3.8 -      (Code_Thingol.empty_funs program3);
     3.9 +    val unimplemented = filter_out (member (op =) abortable)
    3.10 +      (Code_Thingol.unimplemented program3);
    3.11      val _ =
    3.12 -      if null empty_funs then ()
    3.13 +      if null unimplemented then ()
    3.14        else error ("No code equations for " ^
    3.15 -        commas (map (Proof_Context.extern_const ctxt) empty_funs));
    3.16 +        commas (map (Proof_Context.extern_const ctxt) unimplemented));
    3.17      val program4 = Graph.restrict (member (op =) names4) program3;
    3.18    in (names4, program4) end;
    3.19  
    3.20 @@ -500,9 +500,9 @@
    3.21  
    3.22  (* code generation *)
    3.23  
    3.24 -fun transitivly_non_empty_funs thy naming program =
    3.25 +fun implemented_functions thy naming program =
    3.26    let
    3.27 -    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
    3.28 +    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.unimplemented program);
    3.29      val names = map_filter (Code_Thingol.lookup_const naming) cs;
    3.30    in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
    3.31  
    3.32 @@ -510,7 +510,7 @@
    3.33    let
    3.34      val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
    3.35      val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
    3.36 -    val names3 = transitivly_non_empty_funs thy naming program;
    3.37 +    val names3 = implemented_functions thy naming program;
    3.38      val cs3 = map_filter (fn (c, name) =>
    3.39        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    3.40    in union (op =) cs3 cs1 end;
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jan 01 01:05:30 2014 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jan 01 01:05:46 2014 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4    val ensure_declared_const: theory -> string -> naming -> string * naming
     4.5  
     4.6    datatype stmt =
     4.7 -      NoStmt
     4.8 +      NoStmt of string
     4.9      | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    4.10      | Datatype of string * (vname list *
    4.11          ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
    4.12 @@ -81,7 +81,7 @@
    4.13          inst_params: ((string * (const * int)) * (thm * bool)) list,
    4.14          superinst_params: ((string * (const * int)) * (thm * bool)) list };
    4.15    type program = stmt Graph.T
    4.16 -  val empty_funs: program -> string list
    4.17 +  val unimplemented: program -> string list
    4.18    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    4.19    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
    4.20    val is_constr: program -> string -> bool
    4.21 @@ -419,7 +419,7 @@
    4.22  
    4.23  type typscheme = (vname * sort) list * itype;
    4.24  datatype stmt =
    4.25 -    NoStmt
    4.26 +    NoStmt of string
    4.27    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    4.28    | Datatype of string * (vname list * ((string * vname list) * itype list) list)
    4.29    | Datatypecons of string * string
    4.30 @@ -433,8 +433,8 @@
    4.31  
    4.32  type program = stmt Graph.T;
    4.33  
    4.34 -fun empty_funs program =
    4.35 -  Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];
    4.36 +fun unimplemented program =
    4.37 +  Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program [];
    4.38  
    4.39  fun map_terms_bottom_up f (t as IConst _) = f t
    4.40    | map_terms_bottom_up f (t as IVar _) = f t
    4.41 @@ -450,7 +450,7 @@
    4.42  fun map_classparam_instances_as_term f =
    4.43    (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
    4.44  
    4.45 -fun map_terms_stmt f NoStmt = NoStmt
    4.46 +fun map_terms_stmt f (NoStmt c) = (NoStmt c)
    4.47    | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
    4.48        (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
    4.49    | map_terms_stmt f (stmt as Datatype _) = stmt
    4.50 @@ -546,7 +546,7 @@
    4.51        |> pair name
    4.52      else
    4.53        program
    4.54 -      |> Graph.default_node (name, NoStmt)
    4.55 +      |> Graph.default_node (name, NoStmt "")
    4.56        |> add_dep name
    4.57        |> pair naming'
    4.58        |> curry generate (SOME name)
    4.59 @@ -651,17 +651,20 @@
    4.60      fun stmt_classparam class =
    4.61        ensure_class thy algbr eqngr permissive class
    4.62        #>> (fn class => Classparam (c, class));
    4.63 -    fun stmt_fun cert =
    4.64 -      let
    4.65 -        val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    4.66 -        val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
    4.67 -        val some_case_cong = Code.get_case_cong thy c;
    4.68 -      in
    4.69 -        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    4.70 -        ##>> translate_typ thy algbr eqngr permissive ty
    4.71 -        ##>> translate_eqns thy algbr eqngr permissive eqns'
    4.72 -        #>> (fn info => Fun (c, (info, some_case_cong)))
    4.73 -      end;
    4.74 +    fun stmt_fun cert = case Code.equations_of_cert thy cert
    4.75 +     of (_, NONE) => pair (NoStmt c)
    4.76 +      | ((vs, ty), SOME eqns) =>
    4.77 +          let
    4.78 +            val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
    4.79 +            val some_case_cong = Code.get_case_cong thy c;
    4.80 +          in
    4.81 +            fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    4.82 +            ##>> translate_typ thy algbr eqngr permissive ty
    4.83 +            ##>> translate_eqns thy algbr eqngr permissive eqns'
    4.84 +            #>>
    4.85 +             (fn (_, NONE) => NoStmt c
    4.86 +               | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong)))
    4.87 +          end;
    4.88      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    4.89       of SOME (tyco, _) => stmt_datatypecons tyco
    4.90        | NONE => (case Axclass.class_of_param thy c
    4.91 @@ -762,7 +765,6 @@
    4.92    #>> rpair (some_thm, proper)
    4.93  and translate_eqns thy algbr eqngr permissive eqns =
    4.94    maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
    4.95 -  #>> these
    4.96  and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
    4.97    let
    4.98      val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
     5.1 --- a/src/Tools/nbe.ML	Wed Jan 01 01:05:30 2014 +0100
     5.2 +++ b/src/Tools/nbe.ML	Wed Jan 01 01:05:46 2014 +0100
     5.3 @@ -415,7 +415,9 @@
     5.4    IConst { name = c, typargs = [], dicts = dss,
     5.5      dom = [], range = ITyVar "", annotate = false };
     5.6  
     5.7 -fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
     5.8 +fun eqns_of_stmt (_, Code_Thingol.NoStmt _) =
     5.9 +      []
    5.10 +  | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
    5.11        []
    5.12    | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
    5.13        [(const, (vs, map fst eqns))]
    5.14 @@ -519,7 +521,8 @@
    5.15        | is_dict (DFree _) = true
    5.16        | is_dict _ = false;
    5.17      fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
    5.18 -     of Code_Thingol.Fun (c, _) => c
    5.19 +     of Code_Thingol.NoStmt c => c
    5.20 +      | Code_Thingol.Fun (c, _) => c
    5.21        | Code_Thingol.Datatypecons (c, _) => c
    5.22        | Code_Thingol.Classparam (c, _) => c);
    5.23      fun of_apps bounds (t, ts) =