src/Tools/nbe.ML

     | BVar of int * Univ list
     | Abs of (int * (Univ list -> Univ)) * Univ list
   val apps: Univ -> Univ list -> Univ        (*explicit applications*)
   val abss: int -> (Univ list -> Univ) -> Univ
                                              (*abstractions as closures*)
-  val eq_Univ: Univ * Univ -> bool
+  val same: Univ * Univ -> bool
 
   val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
   val trace: bool Unsynchronized.ref
 
   val setup: theory -> theory

         | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
       end
   | apps (Const (name, xs)) ys = Const (name, ys @ xs)
   | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
 
-fun satisfy_abs (abs as ((n, f), xs)) some_k =
-  let
-    val ys = case some_k
-     of NONE => replicate n (BVar (0, []))
-      | SOME k => map_range (fn l => BVar (k + l, [])) n;
-  in (apps (Abs abs) ys, ys) end;
-
-fun maxidx (Const (_, xs)) = fold maxidx xs
-  | maxidx (DFree _) = I
-  | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
-  | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
-
-fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
-  | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
-  | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
-  | eq_Univ (x as Abs abs, y) =
-      let
-        val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
-      in eq_Univ (x, apps y ys) end
-  | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
-  | eq_Univ _ = false;
+fun same (Const (k, xs), Const (l, ys)) = k = l andalso eq_list same (xs, ys)
+  | same (DFree (s, k), DFree (t, l)) = s = t andalso k = l
+  | same (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list same (xs, ys)
+  | same _ = false;
 
 
 (** assembling and compiling ML code from terms **)
 
 (* abstract ML syntax *)

   val name_put =    prefix ^ "put_result";
   val name_ref =    prefix ^ "univs_ref";
   val name_const =  prefix ^ "Const";
   val name_abss =   prefix ^ "abss";
   val name_apps =   prefix ^ "apps";
-  val name_eq =     prefix ^ "eq_Univ";
+  val name_same =     prefix ^ "same";
 in
 
 val univs_cookie = (Univs.get, put_result, name_put);
 
 fun nbe_fun 0 "" = "nbe_value"

   in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
 
 fun nbe_abss 0 f = f `$` ml_list []
   | nbe_abss n f = name_abss `$$` [string_of_int n, f];
 
-fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
+fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
 
 end;
 
 open Basic_Code_Thingol;
 

           (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
         val assemble_rhs = assemble_iterm assemble_constapp match_cont;
         val (samepairs, args') = subst_nonlin_vars args;
         val s_args = map assemble_arg args';
         val s_rhs = if null samepairs then assemble_rhs rhs
-          else ml_if (ml_and (map nbe_eq samepairs))
+          else ml_if (ml_and (map nbe_same samepairs))
             (assemble_rhs rhs) default_rhs;
         val eqns = if is_eval then
             [([ml_list (rev (dicts @ s_args))], s_rhs)]
           else
             [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),