1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4     lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
     1.5  
     1.6  ML {*
     1.7 -open Sledgehammer_Filter_MaSh
     1.8  open MaSh_Export
     1.9  *}
    1.10  
    1.11 @@ -26,7 +25,7 @@
    1.12  
    1.13  ML {*
    1.14  if do_it then
    1.15 -  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
    1.16 +  generate_accessibility thy false "/tmp/mash_accessibility"
    1.17  else
    1.18    ()
    1.19  *}
    1.20 @@ -40,7 +39,7 @@
    1.21  
    1.22  ML {*
    1.23  if do_it then
    1.24 -  generate_isa_dependencies @{context} thy false "/tmp/mash_isa_dependencies"
    1.25 +  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    1.26  else
    1.27    ()
    1.28  *}