src/HOL/Statespace/state_space.ML

 (*  Title:      HOL/Statespace/state_space.ML
-    Author:     Norbert Schirmer, TU Muenchen
+    Author:     Norbert Schirmer, TU Muenchen, 2007
+    Author:     Norbert Schirmer, Apple, 2021
 *)
 
 signature STATE_SPACE =
 sig
   val distinct_compsN : string

         Syntax.free (project_name T) $ Syntax.free n $ s
   | NONE =>
       if get_silent (Context.Proof ctxt)
       then Syntax.const \<^const_name>\<open>StateFun.lookup\<close> $
         Syntax.const \<^const_syntax>\<open>undefined\<close> $ Syntax.free n $ s
-      else (trace_name_space_data (Context.Proof ctxt);
-            raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", [])));
+      else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []));
 
 fun lookup_tr ctxt [s, x] =
   (case Term_Position.strip_positions x of
     Free (n,_) => gen_lookup_tr ctxt s n
   | _ => raise Match);