src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35021 c839a4c670c6
parent 34974 18b41bba42b5
child 35060 6088dfd5f9c8
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -180,7 +180,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 Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     1.8 +val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
     1.9  
    1.10  (* ----- generating beta reduction rules from definitions-------------------- *)
    1.11  
    1.12 @@ -263,7 +263,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 -    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.17 +    Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.18  end;
    1.19  
    1.20  local 
    1.21 @@ -554,7 +554,7 @@
    1.22          flat
    1.23            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    1.24          distincts cs;
    1.25 -  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
    1.26 +  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
    1.27  
    1.28  local 
    1.29    fun pgterm rel con args =
    1.30 @@ -755,7 +755,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 Drule.standard
    1.35 +  val take_rews = map Drule.export_without_context
    1.36      (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
    1.37  end; (* local *)
    1.38