src/HOL/Tools/record.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 32970 fbd2bb2489a8
     1.1 --- a/src/HOL/Tools/record.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -1045,7 +1045,7 @@
     1.4          we varify the proposition manually here.*)
     1.5    else
     1.6      let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
     1.7 -    in if stndrd then standard prf else prf end;
     1.8 +    in if stndrd then Drule.standard prf else prf end;
     1.9  
    1.10  fun quick_and_dirty_prf noopt opt () =
    1.11    if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
    1.12 @@ -1097,7 +1097,7 @@
    1.13            if is_sel_upd_pair thy acc upd
    1.14            then o_eq_dest
    1.15            else o_eq_id_dest;
    1.16 -      in standard (othm RS dest) end;
    1.17 +      in Drule.standard (othm RS dest) end;
    1.18    in map get_simp upd_funs end;
    1.19  
    1.20  fun get_updupd_simp thy defset intros_tac u u' comp =
    1.21 @@ -1118,7 +1118,7 @@
    1.22              REPEAT_DETERM (intros_tac 1),
    1.23              TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
    1.24      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
    1.25 -  in standard (othm RS dest) end;
    1.26 +  in Drule.standard (othm RS dest) end;
    1.27  
    1.28  fun get_updupd_simps thy term defset intros_tac =
    1.29    let
    1.30 @@ -1312,7 +1312,8 @@
    1.31              val ss = get_sel_upd_defs thy;
    1.32              val uathm = get_upd_acc_cong_thm upd acc thy ss;
    1.33            in
    1.34 -            [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
    1.35 +           [Drule.standard (uathm RS updacc_noopE),
    1.36 +            Drule.standard (uathm RS updacc_noop_compE)]
    1.37            end;
    1.38  
    1.39          (*If f is constant then (f o g) = f. we know that K_skeleton
    1.40 @@ -1755,7 +1756,7 @@
    1.41        to prove other theorems. We haven't given names to the accessors
    1.42        f, g etc yet however, so we generate an ext structure with
    1.43        free variables as all arguments and allow the introduction tactic to
    1.44 -      operate on it as far as it can. We then use standard to convert
    1.45 +      operate on it as far as it can. We then use Drule.standard to convert
    1.46        the free variables into unifiable variables and unify them with
    1.47        (roughly) the definition of the accessor.*)
    1.48      fun surject_prf () =
    1.49 @@ -1766,8 +1767,8 @@
    1.50            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
    1.51            REPEAT_ALL_NEW intros_tac 1;
    1.52          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
    1.53 -        val [halfway] = Seq.list_of (tactic1 start);    (* FIXME Seq.lift_of ?? *)
    1.54 -        val [surject] = Seq.list_of (tactic2 (standard halfway));    (* FIXME Seq.lift_of ?? *)
    1.55 +        val [halfway] = Seq.list_of (tactic1 start);  (* FIXME Seq.lift_of ?? *)
    1.56 +        val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));  (* FIXME Seq.lift_of ?? *)
    1.57        in
    1.58          surject
    1.59        end;
    1.60 @@ -2168,14 +2169,14 @@
    1.61      fun sel_convs_prf () =
    1.62        map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
    1.63      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
    1.64 -    fun sel_convs_standard_prf () = map standard sel_convs
    1.65 +    fun sel_convs_standard_prf () = map Drule.standard sel_convs
    1.66      val sel_convs_standard =
    1.67        timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
    1.68  
    1.69      fun upd_convs_prf () =
    1.70        map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
    1.71      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
    1.72 -    fun upd_convs_standard_prf () = map standard upd_convs
    1.73 +    fun upd_convs_standard_prf () = map Drule.standard upd_convs
    1.74      val upd_convs_standard =
    1.75        timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
    1.76  
    1.77 @@ -2183,7 +2184,7 @@
    1.78        let
    1.79          val symdefs = map symmetric (sel_defs @ upd_defs);
    1.80          val fold_ss = HOL_basic_ss addsimps symdefs;
    1.81 -        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
    1.82 +        val ua_congs = map (Drule.standard o simplify fold_ss) upd_acc_cong_assists;
    1.83        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
    1.84      val (fold_congs, unfold_congs) =
    1.85        timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
    1.86 @@ -2217,7 +2218,7 @@
    1.87              [(cterm_of defs_thy Pvar, cterm_of defs_thy
    1.88                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
    1.89              induct_scheme;
    1.90 -        in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
    1.91 +        in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
    1.92  
    1.93      fun cases_scheme_prf_noopt () =
    1.94        prove_standard [] cases_scheme_prop
    1.95 @@ -2262,7 +2263,7 @@
    1.96              rtac (prop_subst OF [surjective]) 1,
    1.97              REPEAT (etac meta_allE 1), atac 1]);
    1.98      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
    1.99 -    fun split_meta_standardise () = standard split_meta;
   1.100 +    fun split_meta_standardise () = Drule.standard split_meta;
   1.101      val split_meta_standard =
   1.102        timeit_msg "record split_meta standard:" split_meta_standardise;
   1.103  
   1.104 @@ -2287,7 +2288,7 @@
   1.105            |> equal_elim (symmetric split_meta') (*!!r. P r*)
   1.106            |> meta_to_obj_all                    (*All r. P r*)
   1.107            |> implies_intr cr                    (* 2 ==> 1 *)
   1.108 -     in standard (thr COMP (thl COMP iffI)) end;
   1.109 +     in Drule.standard (thr COMP (thl COMP iffI)) end;
   1.110  
   1.111      fun split_object_prf_noopt () =
   1.112        prove_standard [] split_object_prop