src/HOL/Statespace/state_fun.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4                              then Bound 2
     1.5                              else raise TERM ("",[n]);
     1.6                     val sel' = lo $ d $ n' $ s;
     1.7 -                  in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
     1.8 +                  in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
     1.9  
    1.10           fun dest_state (s as Bound 0) = s
    1.11             | dest_state (s as (Const (sel,sT)$Bound 0)) =
    1.12 @@ -295,10 +295,10 @@
    1.13             | dest_state s = 
    1.14                      raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
    1.15    
    1.16 -         fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
    1.17 +         fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
    1.18                             ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
    1.19                             (false,Teq,lT,lo,d,n,X,dest_state s)
    1.20 -           | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
    1.21 +           | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
    1.22                              ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
    1.23                             (true,Teq,lT,lo,d,n,X,dest_state s)
    1.24             | dest_sel_eq _ = raise TERM ("",[]);