src/HOL/Statespace/state_space.ML
changeset 30249 9d9145349d19
parent 29390 5c26e3a63b8e
child 30280 eb98b49ef835
     1.1 --- a/src/HOL/Statespace/state_space.ML	Wed Mar 04 13:41:59 2009 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Mar 04 13:42:23 2009 +0100
     1.3 @@ -611,7 +611,7 @@
     1.4             Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
     1.5         | NONE =>
     1.6             if get_silent (Context.Proof ctxt)
     1.7 -	   then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
     1.8 +	   then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
     1.9             else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
    1.10  
    1.11  fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
    1.12 @@ -637,8 +637,8 @@
    1.13        | NONE =>
    1.14           if get_silent (Context.Proof ctxt)
    1.15           then Syntax.const "StateFun.update"$
    1.16 -                   Syntax.const "arbitrary"$Syntax.const "arbitrary"$
    1.17 -                   Syntax.free n$(Syntax.const KN $ v)$s
    1.18 +                   Syntax.const "undefined" $ Syntax.const "undefined" $
    1.19 +                   Syntax.free n $ (Syntax.const KN $ v) $ s
    1.20           else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
    1.21     end;
    1.22