1.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 01 14:35:51 2011 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 01 16:46:07 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  val tests = ["Brackin", "Instructions", "SML", "Verilog"];
     1.6  
     1.7 -timing := true;
     1.8 +Toplevel.timing := true;
     1.9  
    1.10  warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    1.11  use_thys tests;

     2.1 --- a/Admin/Benchmarks/HOL-record/ROOT.ML	Thu Sep 01 14:35:51 2011 +0200
     2.2 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML	Thu Sep 01 16:46:07 2011 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  
     2.5  val tests = ["RecordBenchmark"];
     2.6  
     2.7 -timing := true;
     2.8 +Toplevel.timing := true;
     2.9  
    2.10  warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    2.11  use_thys tests;

     3.1 --- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Thu Sep 01 14:35:51 2011 +0200
     3.2 +++ b/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Thu Sep 01 16:46:07 2011 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -ML {* Record.timing := true *}
     3.8 +declare [[record_timing]]
     3.9  
    3.10  record many_A =
    3.11  A000::nat
    3.12 @@ -313,59 +313,55 @@
    3.13  A299::nat
    3.14  
    3.15  lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
    3.16 -by simp
    3.17 +  by simp
    3.18  
    3.19  lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
    3.20 -by simp
    3.21 +  by simp
    3.22  
    3.23  lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
    3.24 -by simp
    3.25 +  by simp
    3.26  
    3.27  lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
    3.28 -apply (tactic {* simp_tac
    3.29 -          (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*})
    3.30 -done
    3.31 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
    3.32 +  done
    3.33  
    3.34  lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
    3.35 -  apply (tactic {* simp_tac
    3.36 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    3.37 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    3.38    apply simp
    3.39    done
    3.40  
    3.41  lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
    3.42 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.43 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.44    apply simp
    3.45    done
    3.46  
    3.47  lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
    3.48 -  apply (tactic {* simp_tac
    3.49 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    3.50 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    3.51    apply simp
    3.52    done
    3.53  
    3.54  lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
    3.55 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.56 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.57    apply simp
    3.58    done
    3.59  
    3.60  lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
    3.61 -  apply (tactic {* simp_tac
    3.62 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    3.63 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    3.64    apply auto
    3.65    done
    3.66  
    3.67  lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
    3.68 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.69 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.70    apply auto
    3.71    done
    3.72  
    3.73  lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
    3.74 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.75 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.76    apply auto
    3.77    done
    3.78  
    3.79  lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
    3.80 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.81 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.82    apply auto
    3.83    done
    3.84  
    3.85 @@ -378,7 +374,7 @@
    3.86      have "\<exists>x. P x"
    3.87        using pre
    3.88        apply -
    3.89 -      apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    3.90 +      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    3.91        apply auto 
    3.92        done
    3.93    }
    3.94 @@ -387,8 +383,7 @@
    3.95  
    3.96  
    3.97  lemma "\<exists>r. A155 r = x"
    3.98 -  apply (tactic {*simp_tac 
    3.99 -           (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
   3.100 +  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   3.101    done
   3.102  
   3.103