# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1403441256 -7200
# Node ID 137308a1da3c042f5fbd86617599824184ca887b
# Parent  467ccd9ef7d6ea58feaebd40deebdd9d0cfb92e2
ad thehier: removed theory' = Unsychronized.ref

ATTENTION: Test_Isac.thy restored in subsequent changeset

diff -r 467ccd9ef7d6 -r 137308a1da3c src/Tools/isac/Interpret/rewtools.sml
--- a/src/Tools/isac/Interpret/rewtools.sml	Sun Jun 22 14:32:51 2014 +0200
+++ b/src/Tools/isac/Interpret/rewtools.sml	Sun Jun 22 14:47:36 2014 +0200
@@ -361,48 +361,25 @@
     else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)
   end;
 
+(* which theory in ancestors of thy' contains a ruleset *)
+fun thy_containing_rls (thy' : theory') (rls' : rls') =
+  let
+    val thy = Thy_Info.get_theory thy'
+  in
+    case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
+      SOME (thy'', _) => (partID' thy'', thy'')
+    | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
+  end
 
-(* which theory in ancestors of thy' contains a ruleset;
-  i.e. get the occurence _after_ in the _list_ (is up to asking TUM) theory' *)
-local infix mem; (*from Isabelle2002*)
-fun x mem [] = false
-  | x mem (y :: ys) = x = y orelse x mem ys;
-in
-fun thy_containing_rls (thy':theory') (rls':rls') =
+(* this function cannot work as long as the datastructure does not contain thy' *)
+fun thy_containing_cal (thy' : theory') (sop : prog_calcID) =
   let
-    val rls' = strip_thy rls'
-    val thy' = thyID2theory' thy'
-    (*take thys between "Isac" and thy' excluding search for #1#--see calcelems.sml*)
-    val dropthys =
-      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
-        (rev (!theory'))
-		val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
-		(*drop those rulesets which are generated in a theory found in #1#*)
-		val ancestors_rls = 
-		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
-		    (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory thy')))
-  in case assoc (ancestors_rls, rls') of
-	     SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
-	   | _ => error ("thy_containing_rls : rls '" ^ rls' ^
-	     "' not in !rulset' of ancestors of thy '" ^ thy' ^ "'")
-  end;
-
-fun thy_containing_cal (thy':theory') termop =
-  let
-    val thy' = thyID2theory' thy'
-    val dropthys =
-      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
-        (rev (!theory'))
-    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
-    val ancestors_cal =
-      filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
-        (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev)
-  in case assoc (ancestors_cal, strip_thy termop) of
-	     SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
-	   | _ => error ("thy_containing_cal : rls '" ^ termop ^
-			 "' not in KEStore_Elems of ancestors of thy '" ^ thy' ^ "'")
+    val thy = Thy_Info.get_theory thy'
+  in
+    case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
+      SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Atools" (*FIXME*))
+    | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
   end
-end; (*local*)
 
 (*.packing return-values to matchTheory, contextToThy for xml-generation.*)
 datatype contthy =  (*also an item from KEStore on Browser ......#*)
diff -r 467ccd9ef7d6 -r 137308a1da3c src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Sun Jun 22 14:32:51 2014 +0200
+++ b/src/Tools/isac/calcelems.sml	Sun Jun 22 14:47:36 2014 +0200
@@ -424,9 +424,6 @@
   | ketype2str' Pbl_ = "Problem"
   | ketype2str' Met_ = "Method";
 
-(*see 'How to manage theorys in subproblems' at 'type thyID'*)
-val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
-
 (*rewrite orders, also stored in 'type met' and type 'and rls'
   The association list is required for 'rewrite.."rew_ord"..'
   WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)