# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1282140207 -7200
# Node ID 183e35109ddaa28511aa3d7bb0354e8ddd85e544
# Parent  e6fc98fbcb850802ac2ff93f66a4e5632a93681d
resuming after ME/ctree.sml

diff -r e6fc98fbcb85 -r 183e35109dda src/Tools/isac/Isac_Mathengine.thy
--- a/src/Tools/isac/Isac_Mathengine.thy	Wed Aug 18 13:55:23 2010 +0200
+++ b/src/Tools/isac/Isac_Mathengine.thy	Wed Aug 18 16:03:27 2010 +0200
@@ -22,7 +22,6 @@
 begin
 
 ML {* Toplevel.debug := true; *}
-
 use "library.sml"
 use "calcelems.sml"
 ML {* check_guhs_unique := true *}
@@ -35,6 +34,7 @@
 
 use "ME/mstools.sml"
 use "ME/ctree.sml"
+use "ME/ptyps.sml"
 
 
 ML {*
@@ -44,7 +44,6 @@
 
 
 (*
-use "ME/ptyps.sml"
 use "ME/generate.sml"
 use "ME/calchead.sml"
 use "ME/appl.sml"
diff -r e6fc98fbcb85 -r 183e35109dda src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Wed Aug 18 13:55:23 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Wed Aug 18 16:03:27 2010 +0200
@@ -546,8 +546,11 @@
   | assoc' ((keyi, xi) :: pairs, key) =
       if key = keyi then SOME xi else assoc' (pairs, key);
 
-fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
-  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");
+(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
+  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
+fun assoc_thy (thy:theory') = theory 
+  ((implode o (curry takelast 4) o explode) thy);
+
 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
    these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
    overlays by re-using an identifier in different thys.*)