# HG changeset patch
# User haftmann
# Date 1236170543 -3600
# Node ID 9d9145349d1902805011a0f929c8161a016eddd4
# Parent  4f699164ab0c3a367260455b95a951cbf2631180
less arbitrary occurrences of undefined

diff -r 4f699164ab0c -r 9d9145349d19 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Mar 04 13:41:59 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Wed Mar 04 13:42:23 2009 +0100
@@ -611,7 +611,7 @@
            Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
        | NONE =>
            if get_silent (Context.Proof ctxt)
-	   then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
+	   then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
            else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
 
 fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
@@ -637,8 +637,8 @@
       | NONE =>
          if get_silent (Context.Proof ctxt)
          then Syntax.const "StateFun.update"$
-                   Syntax.const "arbitrary"$Syntax.const "arbitrary"$
-                   Syntax.free n$(Syntax.const KN $ v)$s
+                   Syntax.const "undefined" $ Syntax.const "undefined" $
+                   Syntax.free n $ (Syntax.const KN $ v) $ s
          else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
    end;