# HG changeset patch
# User wenzelm
# Date 1230909670 -3600
# Node ID 18a8b7e14a2a6cac7b242c700d4ac2a86be31b26
# Parent  6852248da4b4b901e33f43dbb6371323598df026
tuned;

diff -r 6852248da4b4 -r 18a8b7e14a2a src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Fri Jan 02 15:44:59 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Fri Jan 02 16:21:10 2009 +0100
@@ -40,15 +40,6 @@
 type id = string;
 val no_id : id = "";
 
-fun identify tr =
-  (case Toplevel.get_id tr of
-    SOME id => (id, tr)
-  | NONE =>
-      let val id =
-        if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of tr ^ serial_string ()
-        else "isabelle:" ^ serial_string ()
-      in (id, Toplevel.put_id id tr) end);
-
 
 (* command category *)
 
@@ -167,7 +158,15 @@
 
 fun create_command raw_tr =
   let
-    val (id, tr) = identify raw_tr;
+    val (id, tr) =
+      (case Toplevel.get_id raw_tr of
+        SOME id => (id, raw_tr)
+      | NONE =>
+          let val id =
+            if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
+            else "isabelle:" ^ serial_string ()
+          in (id, Toplevel.put_id id raw_tr) end);
+
     val cmd = make_command (category_of tr, tr, Unprocessed);
     val _ = change_commands (Graph.new_node (id, cmd));
   in id end;