# HG changeset patch
# User huffman
# Date 1235333000 28800
# Node ID eb9bdc4292be492b50a485820dee6858b3f88e50
# Parent  84205156ca8a602052bc7606dfacda44d5984746# Parent  ace8a0847002eb89c182580f746bc9deaeb2a266
merged

diff -r 84205156ca8a -r eb9bdc4292be src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/HOL/Library/Primes.thy	Sun Feb 22 12:03:20 2009 -0800
@@ -45,12 +45,14 @@
   by (rule prime_dvd_square) (simp_all add: power2_eq_square)
 
 
-lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto)
+lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0"
+by (induct n, auto)
+
 lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y"
-  using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"]
-    by auto
+by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base)
+
 lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y"
-  by (simp only: linorder_not_less[symmetric] exp_mono_lt)
+by (simp only: linorder_not_less[symmetric] exp_mono_lt)
 
 lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y"
 using power_inject_base[of x n y] by auto
diff -r 84205156ca8a -r eb9bdc4292be src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/HOL/Nat.thy	Sun Feb 22 12:03:20 2009 -0800
@@ -735,6 +735,11 @@
   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
 qed
 
+instance nat :: no_zero_divisors
+proof
+  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+qed
+
 lemma nat_mult_1: "(1::nat) * n = n"
 by simp
 
diff -r 84205156ca8a -r eb9bdc4292be src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/HOL/Parity.thy	Sun Feb 22 12:03:20 2009 -0800
@@ -228,20 +228,9 @@
 
 lemma zero_le_odd_power: "odd n ==>
     (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
-  apply (simp add: odd_nat_equiv_def2)
-  apply (erule exE)
-  apply (erule ssubst)
-  apply (subst power_Suc)
-  apply (subst power_add)
-  apply (subst zero_le_mult_iff)
-  apply auto
-  apply (subgoal_tac "x = 0 & y > 0")
-  apply (erule conjE, assumption)
-  apply (subst power_eq_0_iff [symmetric])
-  apply (subgoal_tac "0 <= x^y * x^y")
-  apply simp
-  apply (rule zero_le_square)+
-  done
+apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
+apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
+done
 
 lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
     (even n | (odd n & 0 <= x))"
diff -r 84205156ca8a -r eb9bdc4292be src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/HOL/Power.thy	Sun Feb 22 12:03:20 2009 -0800
@@ -143,11 +143,13 @@
 done
 
 lemma power_eq_0_iff [simp]:
-  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
+  "(a^n = 0) \<longleftrightarrow>
+   (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
 apply (induct "n")
-apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
+apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
 done
 
+
 lemma field_power_not_zero:
   "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
 by force
@@ -370,6 +372,13 @@
 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
 by (induct "n", auto)
 
+lemma nat_power_eq_Suc_0_iff [simp]: 
+  "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
+by (induct_tac m, auto)
+
+lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
+by simp
+
 text{*Valid for the naturals, but what if @{text"0<i<1"}?
 Premises cannot be weakened: consider the case where @{term "i=0"},
 @{term "m=1"} and @{term "n=0"}.*}
diff -r 84205156ca8a -r eb9bdc4292be src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/Pure/Isar/code.ML	Sun Feb 22 12:03:20 2009 -0800
@@ -489,7 +489,7 @@
 
 fun retrieve_algebra thy operational =
   Sorts.subalgebra (Syntax.pp_global thy) operational
-    (arity_constraints thy (Sign.classes_of thy))
+    (SOME o arity_constraints thy (Sign.classes_of thy))
     (Sign.classes_of thy);
 
 in
diff -r 84205156ca8a -r eb9bdc4292be src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/Pure/sorts.ML	Sun Feb 22 12:03:20 2009 -0800
@@ -48,7 +48,7 @@
   val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
   val classrels_of: algebra -> (class * class list) list
   val instances_of: algebra -> (string * class) list
-  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
+  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
   val class_error: Pretty.pp -> class_error -> string
@@ -322,9 +322,10 @@
   let
     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
     fun restrict_arity tyco (c, (_, Ss)) =
-      if P c then
-        SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
+      if P c then case sargs (c, tyco)
+       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
           |> map restrict_sort))
+        | NONE => NONE
       else NONE;
     val classes' = classes |> Graph.subgraph P;
     val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
diff -r 84205156ca8a -r eb9bdc4292be src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Sun Feb 22 10:53:10 2009 -0800
+++ b/src/Tools/code/code_wellsorted.ML	Sun Feb 22 12:03:20 2009 -0800
@@ -1,7 +1,7 @@
 (*  Title:      Tools/code/code_wellsorted.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Retrieving, well-sorting and structuring code equations in graph
+Producing well-sorted systems of code equations in a graph
 with explicit dependencies -- the Waisenhaus algorithm.
 *)
 
@@ -81,19 +81,25 @@
 structure Vargraph =
   GraphFun(type key = var val ord = prod_ord const_ord int_ord);
 
-datatype styp = Tyco of string * styp list | Var of var;
+datatype styp = Tyco of string * styp list | Var of var | Free;
+
+fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
+  | styp_of c_lhs (TFree (v, _)) = case c_lhs
+     of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
+      | NONE => Free;
 
-val empty_vardeps : ((string * styp list) list * class list) Vargraph.T
-    * (const list * ((string * sort) list * (thm * bool) list) Symtab.table) =
-  (Vargraph.empty, ([], Symtab.empty));
-  (*FIXME: user table with proto equations as assertor for functions,
-    add dummy to styp which allows to process consts of terms directly*)
+type vardeps_data = ((string * styp list) list * class list) Vargraph.T
+  * (((string * sort) list * (thm * bool) list) Symtab.table
+    * (class * string) list);
 
-(* computing instantiations *)
+val empty_vardeps_data : vardeps_data =
+  (Vargraph.empty, (Symtab.empty, []));
+
+(* retrieving equations and instances from the background context *)
 
 fun obtain_eqns thy eqngr c =
   case try (Graph.get_node eqngr) c
-   of SOME ((lhs, _), eqns) => ((lhs, []), eqns)
+   of SOME ((lhs, _), eqns) => ((lhs, []), [])
     | NONE => let
         val eqns = Code.these_eqns thy c
           |> burrow_fst (Code_Unit.norm_args thy)
@@ -112,6 +118,9 @@
         val inst_params = inst_params thy tyco all_classes;
       in (classess, (superclasses, inst_params)) end;
 
+
+(* computing instantiations *)
+
 fun add_classes thy arities eqngr c_k new_classes vardeps_data =
   let
     val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
@@ -122,7 +131,7 @@
   in
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
-    |> fold (fn styp => fold (add_typmatch_inst thy arities eqngr styp) new_classes) styps
+    |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps
     |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
   end end
 and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
@@ -132,7 +141,7 @@
   else
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
-    |> fold (add_typmatch_inst thy arities eqngr tyco_styps) classes
+    |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes
   end
 and add_dep thy arities eqngr c_k c_k' vardeps_data =
   let
@@ -142,27 +151,23 @@
     |> add_classes thy arities eqngr c_k' classes
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
-and add_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
+and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
   if can (Sign.arity_sorts thy tyco) [class]
   then vardeps_data
-    |> assert thy arities eqngr (Inst (class, tyco))
+    |> assert_inst thy arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
-         add_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+         assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
   else vardeps_data (*permissive!*)
-and add_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
-      vardeps_data
-      |> add_dep thy arities eqngr c_k c_k'
-  | add_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
-      vardeps_data
-      |> add_styp thy arities eqngr c_k tyco_styps
-and add_inst thy arities eqngr (inst as (class, tyco)) vardeps_data =
-  let
+and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+  if member (op =) insts inst then vardeps_data
+  else let
     val (classess, (superclasses, inst_params)) =
       obtain_instance thy arities inst;
   in
     vardeps_data
-    |> fold (fn superclass => assert thy arities eqngr (Inst (superclass, tyco))) superclasses
-    |> fold (assert thy arities eqngr o Fun) inst_params
+    |> (apsnd o apsnd) (insert (op =) inst)
+    |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
+    |> fold (assert_fun thy arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
          #> add_classes thy arities eqngr (Inst (class, tyco), k) classes
@@ -175,27 +180,32 @@
              ) inst_params
          ) classess
   end
-and add_const thy arities eqngr c vardeps_data =
-  let
+and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+      vardeps_data
+      |> add_styp thy arities eqngr c_k tyco_styps
+  | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+      vardeps_data
+      |> add_dep thy arities eqngr c_k c_k'
+  | assert_typmatch thy arities eqngr Free c_k vardeps_data =
+      vardeps_data
+and assert_rhs thy arities eqngr (c', styps) vardeps_data =
+  vardeps_data
+  |> assert_fun thy arities eqngr c'
+  |> fold_index (fn (k, styp) =>
+       assert_typmatch thy arities eqngr styp (Fun c', k)) styps
+and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+  if Symtab.defined eqntab c then vardeps_data
+  else let
     val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
-    fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
-      | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
-    val rhss' = (map o apsnd o map) styp_of rhss;
+    val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   in
     vardeps_data
-    |> (apsnd o apsnd) (Symtab.update_new (c, (lhs, eqns)))
+    |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
     |> fold_index (fn (k, (_, sort)) =>
          apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))
          #> add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
-    |> fold (assert thy arities eqngr o Fun o fst) rhss'
-    |> fold (fn (c', styps) => fold_index (fn (k', styp) =>
-         add_typmatch thy arities eqngr styp (Fun c', k')) styps) rhss'
-  end
-and assert thy arities eqngr c vardeps_data =
-  if member (op =) ((fst o snd) vardeps_data) c then vardeps_data
-  else case c
-   of Fun const => vardeps_data |> (apsnd o apfst) (cons c) |> add_const thy arities eqngr const
-    | Inst inst => vardeps_data |> (apsnd o apfst) (cons c) |> add_inst thy arities eqngr inst;
+    |> fold (assert_rhs thy arities eqngr) rhss'
+  end;
 
 
 (* applying instantiations *)
@@ -209,16 +219,14 @@
       |> filter (is_proper o fst)
       |> (map o apsnd) (filter is_proper);
     val instances = Sorts.instances_of thy_algebra
-      |> filter (is_proper o snd);
+      |> filter (is_proper o snd)
+      |> map swap (*FIXME*)
     fun add_class (class, superclasses) algebra =
       Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
-    fun add_arity (tyco, class) algebra =
-      case AList.lookup (op =) arities (tyco, class)
-       of SOME sorts => Sorts.add_arities pp
-            (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
-        | NONE => if Sign.arity_number thy tyco = 0
-            then Sorts.add_arities pp (tyco, [(class, [])]) algebra
-            else algebra;
+    fun add_arity (class, tyco) algebra = case AList.lookup (op =) arities (class, tyco)
+     of SOME sorts => Sorts.add_arities pp
+         (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
+      | NONE => algebra;
   in
     Sorts.empty_algebra
     |> fold add_class classrels
@@ -229,7 +237,8 @@
   let
     fun class_relation (x, _) _ = x;
     fun type_constructor tyco xs class =
-      inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs;
+      inst_params thy tyco (Sorts.complete_sort algebra [class])
+        @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
     flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
@@ -238,74 +247,46 @@
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;
 
-fun add_arities thy vardeps = Vargraph.fold (fn ((Fun _, _), _) => I
-  | ((Inst (class, tyco), k), ((_, classes), _)) =>
-      AList.map_default (op =)
-        ((tyco, class), replicate (Sign.arity_number thy tyco) [])
-          (nth_map k (K classes))) vardeps;
+fun add_arity thy vardeps (class, tyco) =
+  AList.default (op =)
+    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
+      (0 upto Sign.arity_number thy tyco - 1));
 
-fun add_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
-  let
-    val (proto_lhs, proto_eqns) = (the o Symtab.lookup eqntab) c;
+fun add_eqs thy (proj_sort, algebra) vardeps
+    (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
+  if can (Graph.get_node eqngr) c then (rhss, eqngr)
+  else let
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
       Vartab.update ((v, 0), sort)) lhs;
     val eqns = proto_eqns
       |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
-    val (tyscm, rhss) = tyscm_rhss_of thy c eqns;
-  in
-    gr
-    |> Graph.new_node (c, (tyscm, eqns))
-    |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c'
-        #-> (fn (vs, _) =>
-          fold2 (ensure_match thy (proj_sort, algebra) eqntab vardeps c) Ts (map snd vs))) rhss
-    |> pair tyscm
-  end
-and ensure_match thy (proj_sort, algebra) eqntab vardeps c T sort gr =
-  gr
-  |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' #> snd)
-       (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
-and ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' gr =
-  gr
-  |> ensure_eqs thy (proj_sort, algebra) eqntab vardeps c'
-  ||> Graph.add_edge (c, c')
-and ensure_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
-  case try (Graph.get_node gr) c
-   of SOME (tyscm, _) => (tyscm, gr)
-    | NONE => add_eqs thy (proj_sort, algebra) eqntab vardeps c gr;
+    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
+    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
+  in (map (pair c) rhss' @ rhss, eqngr') end;
 
-fun extend_arities_eqngr thy cs insts (arities, eqngr) =
+fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
   let
-    val (vardeps, (_, eqntab)) = empty_vardeps
-      |> fold (assert thy arities eqngr o Fun) cs
-      |> fold (assert thy arities eqngr o Inst) insts;
-    val arities' = add_arities thy vardeps arities;
+    val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+    val (vardeps, (eqntab, insts)) = empty_vardeps_data
+      |> fold (assert_fun thy arities eqngr) cs
+      |> fold (assert_rhs thy arities eqngr) cs_rhss';
+    val arities' = fold (add_arity thy vardeps) insts arities;
     val algebra = build_algebra thy arities';
     val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
-    fun complete_inst_params (class, tyco) =
-      inst_params thy tyco (Sorts.complete_sort algebra [class]);
-    val cs' = maps complete_inst_params insts @ cs; (*FIXME*)
-    val (_, eqngr') =
-      fold_map (ensure_eqs thy (proj_sort, algebra) eqntab vardeps) cs' eqngr;
-  in ((proj_sort, algebra), (arities', eqngr')) end;
+    val (rhss, eqngr') = Symtab.fold
+      (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
+    fun deps_of (c, rhs) = c ::
+      maps (dicts_of thy (proj_sort, algebra))
+        (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+    val eqngr'' = fold (fn (c, rhs) => fold
+      (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
+  in ((proj_sort, algebra), (arities', eqngr'')) end;
 
 
 (** retrieval interfaces **)
 
-fun instance_dicts_of thy (proj_sort, algebra) (T, sort) = (*FIXME vs. consts_dicts_of *)
-  let
-    fun class_relation (x, _) _ = x;
-    fun type_constructor tyco xs class =
-      (class, tyco) :: (maps o maps) fst xs;
-    fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
-  in
-    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
-      { class_relation = class_relation, type_constructor = type_constructor,
-        type_variable = type_variable } (T, proj_sort sort)
-       handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
-  end;
-
 fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
   let
     val ct = cterm_of proto_ct;
@@ -316,18 +297,17 @@
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
     val t' = Thm.term_of ct';
+    val (t'', evaluator_eqngr) = evaluator t';
     val consts = map fst (consts_of t');
-    val (algebra', arities_eqngr') = extend_arities_eqngr thy consts [] arities_eqngr;
-    val (t'', evaluator_eqngr) = evaluator t';
     val consts' = consts_of t'';
-    val const_matches = fold (fn (c, ty) =>
-      insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
-    val typ_matches = maps (fn (tys, c) =>
-      tys ~~ map snd (fst (fst (Graph.get_node (snd arities_eqngr') c))))
-      const_matches;
-    val insts = maps (instance_dicts_of thy algebra') typ_matches;
-    val (algebra'', arities_eqngr'') = extend_arities_eqngr thy [] insts arities_eqngr';
-  in (evaluator_lift (evaluator_eqngr algebra'') thm (snd arities_eqngr''), arities_eqngr'') end;
+    val const_matches' = fold (fn (c, ty) =>
+      insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
+    val (algebra', arities_eqngr') =
+      extend_arities_eqngr thy consts const_matches' arities_eqngr;
+  in
+    (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
+      arities_eqngr')
+  end;
 
 fun proto_eval_conv thy =
   let