# HG changeset patch
# User wenzelm
# Date 1631288138 -7200
# Node ID 6876e3d5e3625b448327d19636d909922766b7f9
# Parent  8d1e27a23dd1031aa33003f6217c06a8dfe05c1c
unused;

diff -r 8d1e27a23dd1 -r 6876e3d5e362 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Sep 10 15:57:09 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Sep 10 17:35:38 2021 +0200
@@ -35,9 +35,6 @@
   val definition: (binding * typ option * mixfix) option ->
     (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
     local_theory -> (term * (string * thm)) * local_theory
-  val definition': (binding * typ option * mixfix) option ->
-    (binding * typ option * mixfix) list ->  term list -> Attrib.binding * term ->
-    bool -> local_theory -> (term * (string * thm)) * local_theory
   val definition_cmd: (binding * string option * mixfix) option ->
     (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
     bool -> local_theory -> (term * (string * thm)) * local_theory
@@ -262,7 +259,6 @@
           else
             error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
               Position.here (Binding.pos_of b)));
-    val const_name = Local_Theory.full_name lthy b;
 
     val name = Thm.def_binding_optional b a;
     val ((lhs, (_, raw_th)), lthy2) = lthy
@@ -284,8 +280,7 @@
         (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
   in ((lhs, (def_name, th')), lthy5) end;
 
-val definition' = gen_def check_spec_open (K I);
-fun definition xs ys As B = definition' xs ys As B false;
+fun definition xs ys As B = gen_def check_spec_open (K I) xs ys As B false;
 val definition_cmd = gen_def read_spec_open Attrib.check_src;