1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 19 15:51:03 2013 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Sep 20 15:26:24 2013 +0200
     1.3 @@ -1,20 +1,15 @@
     1.4 -(* Title:  functions on lists for Scripts
     1.5 +(* Title:  functions on lists for Programs
     1.6     Author: Walther Neuper 0108
     1.7     (c) due to copyright terms
     1.8  *)
     1.9  
    1.10 -theory ListC imports Complex_Main
    1.11 -uses ("~~/src/Tools/isac/library.sml")
    1.12 -     ("~~/src/Tools/isac/calcelems.sml")
    1.13 -     ("~~/src/Tools/isac/ProgLang/termC.sml") 
    1.14 -     ("~~/src/Tools/isac/ProgLang/calculate.sml") 
    1.15 -     ("~~/src/Tools/isac/ProgLang/rewrite.sml")
    1.16 +theory ListC 
    1.17 +imports Complex_Main "~~/src/Tools/isac/KEStore"
    1.18  begin
    1.19 -use "~~/src/Tools/isac/library.sml"
    1.20 -use "~~/src/Tools/isac/calcelems.sml"
    1.21 -use "~~/src/Tools/isac/ProgLang/termC.sml"
    1.22 -use "~~/src/Tools/isac/ProgLang/calculate.sml"
    1.23 -use "~~/src/Tools/isac/ProgLang/rewrite.sml"
    1.24 +
    1.25 +ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
    1.26 +ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
    1.27 +ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
    1.28  
    1.29  text {* 'nat' in List.thy replaced by 'real' *}
    1.30  
    1.31 @@ -200,4 +195,8 @@
    1.32    [("list_rls",list_rls)
    1.33     ]);
    1.34  *}
    1.35 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
    1.36 +
    1.37 +ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF  Theory_Data*)*}
    1.38 +
    1.39  end

     2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Sep 19 15:51:03 2013 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Fri Sep 20 15:26:24 2013 +0200
     2.3 @@ -483,7 +483,7 @@
     2.4        ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
     2.5  
     2.6  fun instantiate_rls' thy' subs (rls:rls') = 
     2.7 -    rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
     2.8 +    rls2rls' (instantiate_rls subs (assoc_rls rls)) : rlsdat';
     2.9  
    2.10  ... problem with these functions: 
    2.11  > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";