diff -r 139b257e10d2 -r 551eacf071d7 Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Tue Feb 09 14:32:37 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Tue Feb 09 15:28:15 2010 +0100 @@ -105,62 +105,62 @@ by (auto simp add: equivp_def expand_fun_eq) ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "nat \ nat"}, @{typ "myint"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a * 'a) list"}, @{typ "'a foo"}) *} ML {* -test_funs repF @{context} +test_funs RepF @{context} (@{typ "(('a * 'a) list * 'b)"}, @{typ "('a foo * 'b)"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(('a list) * int) list"}, @{typ "('a fset) bar"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list)"}, @{typ "('a fset)"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "((nat * nat) list) list"}, @{typ "((myint) fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(('a * 'a) list) list"}, @{typ "(('a * 'a) fset) fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "(nat * nat) list"}, @{typ "myint fset"}) *} ML {* -test_funs absF @{context} +test_funs AbsF @{context} (@{typ "('a list) list \ 'a list"}, @{typ "('a fset) fset \ 'a fset"}) *}