src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
     1.5  val abs_defin' = iso_locale RS iso_abs_defin';
     1.6  val rep_defin' = iso_locale RS iso_rep_defin';
     1.7 -val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     1.8 +val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     1.9  
    1.10  (* ----- generating beta reduction rules from definitions-------------------- *)
    1.11  
    1.12 @@ -251,7 +251,7 @@
    1.13    val exhaust = pg con_appls (mk_trp exh) (K tacs);
    1.14    val _ = trace " Proving casedist...";
    1.15    val casedist =
    1.16 -    standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.17 +    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.18  end;
    1.19  
    1.20  local 
    1.21 @@ -542,7 +542,7 @@
    1.22          flat
    1.23            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    1.24          distincts cs;
    1.25 -  in map standard (distincts (cons ~~ distincts_le)) end;
    1.26 +  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
    1.27  
    1.28  local 
    1.29    fun pgterm rel con args =
    1.30 @@ -738,7 +738,7 @@
    1.31          maps (eq_tacs ctxt) eqs;
    1.32      in pg copy_take_defs goal tacs end;
    1.33  in
    1.34 -  val take_rews = map standard
    1.35 +  val take_rews = map Drule.standard
    1.36      (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
    1.37  end; (* local *)
    1.38