src/HOL/UNITY/Follows.ML

 \    ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))";
 by Auto_tac;
 by (dres_inst_tac [("x","f xa")] spec 1);
 by (dres_inst_tac [("x","g xa")] spec 1);
 by (ball_tac 1);
-by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
+by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
 qed "increasing_union";
 
 Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
     "[| F : Increasing f;  F: Increasing g |] \
 \    ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))";
 by Auto_tac;
 by (dres_inst_tac [("x","f xa")] spec 1);
 by (dres_inst_tac [("x","g xa")] spec 1);
 by (ball_tac 1);
-by (blast_tac (claset()  addIs [union_le_mono, order_trans]) 1);
+by (blast_tac (claset()  addIs [thm "union_le_mono", order_trans]) 1);
 qed "Increasing_union";
 
 Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
 \     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset()  addIs [union_le_mono]) 1);
+by (blast_tac (claset()  addIs [thm "union_le_mono"]) 1);
 qed "Always_union";
 
 (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
 Goal "[| F : Increasing f; F : Increasing g; \
 \        F : Increasing g'; F : Always {s. f' s <= f s};\

 by (rtac PSP_Stable 1);
 by (eres_inst_tac [("x", "f s")] spec 1);
 by (etac Stable_Int 1);
 by (assume_tac 1);
 by (Blast_tac 1);
-by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
+by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
 qed "Follows_union_lemma";
 
 (*The !! is there to influence to effect of permutative rewriting at the end*)
 Goalw [Follows_def]
      "!!g g' ::'b => ('a::order) multiset. \

 by (asm_full_simp_tac (simpset() addsimps [Increasing_union, Always_union]) 1);
 by Auto_tac;
 by (rtac LeadsTo_Trans 1);
 by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
 (*now exchange union's arguments*)
-by (simp_tac (simpset() addsimps [union_commute]) 1); 
+by (simp_tac (simpset() addsimps [thm "union_commute"]) 1); 
 by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
 qed "Follows_union";
 
 Goal "!!f ::['c,'b] => ('a::order) multiset. \
 \       [| ALL i: I. F : f' i Fols f i;  finite I |] \