# HG changeset patch
# User wenzelm
# Date 936213383 -7200
# Node ID a98963d70f8122c1fb4a40740df5f708447c41fd
# Parent  bd819d0255e15ce40fcfc38e8dcf6a8f9fade10e
Thm.def_name;

diff -r bd819d0255e1 -r a98963d70f81 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Sep 01 21:15:52 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Sep 01 21:16:23 1999 +0200
@@ -20,13 +20,14 @@
 val refl_tac = Tactic.rtac (standard (Drule.reflexive_thm RS Drule.triv_goal));
 
 
-fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
+fun gen_def fix prep_term match_binds raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
   let
     fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
 
-    val state' = fix [(x, raw_T)] state;
+    val state' = fix [([x], raw_T)] state;
     val ctxt' = Proof.context_of state';
 
+    val name = if raw_name = "" then Thm.def_name x else raw_name;
     val rhs = prep_term ctxt' raw_rhs;
     val T = Term.fastype_of rhs;
     val lhs = ProofContext.cert_term ctxt' (Free (x, T));