1.1 --- a/src/Tools/isac/calcelems.sml Tue Oct 05 08:35:55 2010 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Tue Oct 05 09:01:30 2010 +0200
1.3 @@ -552,8 +552,7 @@
1.4 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.5 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
1.6 fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
1.7 - (theory ((implode o (curry takelast 4) o explode) thy))
1.8 - handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.9 + (theory thy) handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.10
1.11 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.12 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle