1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Sun Jun 22 14:32:51 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Sun Jun 22 14:47:36 2014 +0200
     1.3 @@ -361,48 +361,25 @@
     1.4      else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)
     1.5    end;
     1.6  
     1.7 +(* which theory in ancestors of thy' contains a ruleset *)
     1.8 +fun thy_containing_rls (thy' : theory') (rls' : rls') =
     1.9 +  let
    1.10 +    val thy = Thy_Info.get_theory thy'
    1.11 +  in
    1.12 +    case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
    1.13 +      SOME (thy'', _) => (partID' thy'', thy'')
    1.14 +    | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
    1.15 +  end
    1.16  
    1.17 -(* which theory in ancestors of thy' contains a ruleset;
    1.18 -  i.e. get the occurence _after_ in the _list_ (is up to asking TUM) theory' *)
    1.19 -local infix mem; (*from Isabelle2002*)
    1.20 -fun x mem [] = false
    1.21 -  | x mem (y :: ys) = x = y orelse x mem ys;
    1.22 -in
    1.23 -fun thy_containing_rls (thy':theory') (rls':rls') =
    1.24 +(* this function cannot work as long as the datastructure does not contain thy' *)
    1.25 +fun thy_containing_cal (thy' : theory') (sop : prog_calcID) =
    1.26    let
    1.27 -    val rls' = strip_thy rls'
    1.28 -    val thy' = thyID2theory' thy'
    1.29 -    (*take thys between "Isac" and thy' excluding search for #1#--see calcelems.sml*)
    1.30 -    val dropthys =
    1.31 -      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
    1.32 -        (rev (!theory'))
    1.33 -		val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
    1.34 -		(*drop those rulesets which are generated in a theory found in #1#*)
    1.35 -		val ancestors_rls = 
    1.36 -		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
    1.37 -		    (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory thy')))
    1.38 -  in case assoc (ancestors_rls, rls') of
    1.39 -	     SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
    1.40 -	   | _ => error ("thy_containing_rls : rls '" ^ rls' ^
    1.41 -	     "' not in !rulset' of ancestors of thy '" ^ thy' ^ "'")
    1.42 -  end;
    1.43 -
    1.44 -fun thy_containing_cal (thy':theory') termop =
    1.45 -  let
    1.46 -    val thy' = thyID2theory' thy'
    1.47 -    val dropthys =
    1.48 -      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
    1.49 -        (rev (!theory'))
    1.50 -    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
    1.51 -    val ancestors_cal =
    1.52 -      filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
    1.53 -        (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev)
    1.54 -  in case assoc (ancestors_cal, strip_thy termop) of
    1.55 -	     SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
    1.56 -	   | _ => error ("thy_containing_cal : rls '" ^ termop ^
    1.57 -			 "' not in KEStore_Elems of ancestors of thy '" ^ thy' ^ "'")
    1.58 +    val thy = Thy_Info.get_theory thy'
    1.59 +  in
    1.60 +    case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
    1.61 +      SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Atools" (*FIXME*))
    1.62 +    | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
    1.63    end
    1.64 -end; (*local*)
    1.65  
    1.66  (*.packing return-values to matchTheory, contextToThy for xml-generation.*)
    1.67  datatype contthy =  (*also an item from KEStore on Browser ......#*)

     2.1 --- a/src/Tools/isac/calcelems.sml	Sun Jun 22 14:32:51 2014 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Sun Jun 22 14:47:36 2014 +0200
     2.3 @@ -424,9 +424,6 @@
     2.4    | ketype2str' Pbl_ = "Problem"
     2.5    | ketype2str' Met_ = "Method";
     2.6  
     2.7 -(*see 'How to manage theorys in subproblems' at 'type thyID'*)
     2.8 -val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
     2.9 -
    2.10  (*rewrite orders, also stored in 'type met' and type 'and rls'
    2.11    The association list is required for 'rewrite.."rew_ord"..'
    2.12    WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)