repaired assoc_thy isac-update-Isa09-2
authorWalther Neuper <neuper@ist.tugraz.at>
Tue, 05 Oct 2010 09:01:30 +0200
branchisac-update-Isa09-2
changeset 3804226f3832d96b2
parent 38041 850aaf5b3744
child 38043 6a36acec95d9
repaired assoc_thy

such that assoc_thy "Rational" works.
There are related TODOs: fun theory'2thyID, ??
src/Tools/isac/calcelems.sml
     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