src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -168,7 +168,7 @@
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
 val abs_defin' = iso_locale RS iso_abs_defin';
 val rep_defin' = iso_locale RS iso_rep_defin';
-val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
 
 (* ----- generating beta reduction rules from definitions-------------------- *)
 
@@ -251,7 +251,7 @@
   val exhaust = pg con_appls (mk_trp exh) (K tacs);
   val _ = trace " Proving casedist...";
   val casedist =
-    standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
+    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
 end;
 
 local 
@@ -542,7 +542,7 @@
         flat
           (ListPair.map (distinct c) ((map #1 cs),leqs)) @
         distincts cs;
-  in map standard (distincts (cons ~~ distincts_le)) end;
+  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
 
 local 
   fun pgterm rel con args =
@@ -738,7 +738,7 @@
         maps (eq_tacs ctxt) eqs;
     in pg copy_take_defs goal tacs end;
 in
-  val take_rews = map standard
+  val take_rews = map Drule.standard
     (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
 end; (* local *)