diff -r 3e53081ad53a -r c7eff9882bd8 QuotMain.thy --- a/QuotMain.thy Sat Oct 24 22:52:23 2009 +0200 +++ b/QuotMain.thy Sun Oct 25 00:14:40 2009 +0200 @@ -164,15 +164,6 @@ maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} *} - -ML {* quotdata_lookup @{theory} *} -setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} -ML {* quotdata_lookup @{theory} *} - -ML {* print_quotdata @{context} *} - -ML {* maps_lookup @{theory} @{type_name list} *} - ML {* val no_vars = Thm.rule_attribute (fn context => fn th => let