src/Tools/isac/Interpret/script.sml
changeset 55432 1780e9905d80
parent 52153 26f274076fd2
child 55443 46613d0a9fc9
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Jun 05 18:10:46 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Jun 06 06:50:02 2014 +0200
     1.3 @@ -160,10 +160,6 @@
     1.4  > get [] (eq_str "e_") sss;             [R,R]
     1.5  *)
     1.6  
     1.7 -fun test_negotiable t = 
     1.8 -    member op = (!negotiable) 
     1.9 -           ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t);
    1.10 -
    1.11  (*.get argument of first stactic in a script for init_form.*)
    1.12  fun get_stac thy (h $ body) =
    1.13    let