1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -39,12 +39,6 @@
     1.4  val mash_resetN = "mash_reset"
     1.5  val mash_learnN = "mash_learn"
     1.6  
     1.7 -(* experimental *)
     1.8 -val mash_RESET_N = "mash_RESET"
     1.9 -val mash_ADD_N = "mash_ADD"
    1.10 -val mash_DEL_N = "mash_DEL"
    1.11 -val mash_SUGGEST_N = "mash_SUGGEST"
    1.12 -
    1.13  val auto = Unsynchronized.ref false
    1.14  
    1.15  val _ =
    1.16 @@ -387,14 +381,6 @@
    1.17        mash_reset ()
    1.18      else if subcommand = mash_learnN then
    1.19        () (* TODO: implement *)
    1.20 -    else if subcommand = mash_RESET_N then
    1.21 -      () (* TODO: implement *)
    1.22 -    else if subcommand = mash_ADD_N then
    1.23 -      () (* TODO: implement *)
    1.24 -    else if subcommand = mash_DEL_N then
    1.25 -      () (* TODO: implement *)
    1.26 -    else if subcommand = mash_SUGGEST_N then
    1.27 -      () (* TODO: implement *)
    1.28      else
    1.29        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    1.30    end