# HG changeset patch
# User nipkow
# Date 1353674761 -3600
# Node ID e014009fbd93d8310774535ecc58e4462ce86023
# Parent  1a28109edc6dcf3a67f3e09b747397195d38c913
tuned

diff -r 1a28109edc6d -r e014009fbd93 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Thu Nov 22 22:21:54 2012 +0100
+++ b/src/HOL/IMP/Vars.thy	Fri Nov 23 13:46:01 2012 +0100
@@ -31,7 +31,7 @@
 
 end
 
-value "vars(Plus (V ''x'') (V ''y''))"
+value "vars (Plus (V ''x'') (V ''y''))"
 
 instantiation bexp :: vars
 begin
@@ -46,7 +46,7 @@
 
 end
 
-value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
+value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"
 
 abbreviation
   eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"