1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -542,35 +542,31 @@
     1.4  	      SOME (f',_) =>[rule2tac thy subst thm']
     1.5  	    | NONE => []
     1.6      else (case rewrite_ thy ro erls false thm f of
     1.7 -	SOME (f',_) => [rule2tac thy [] thm']
     1.8 +	      SOME (f',_) => [rule2tac thy [] thm']
     1.9  	    | NONE => [])
    1.10    | try_rew thy _ _ _ f (cal as Calc c) = 
    1.11      (case get_calculation_ thy c f of
    1.12 -	SOME (str, _) => [rule2tac thy [] cal]
    1.13 +	      SOME (str, _) => [rule2tac thy [] cal]
    1.14        | NONE => [])
    1.15    | try_rew thy _ _ _ f (cal as Cal1 c) = 
    1.16      (case get_calculation_ thy c f of
    1.17 -	SOME (str, _) => [rule2tac thy [] cal]
    1.18 +	      SOME (str, _) => [rule2tac thy [] cal]
    1.19        | NONE => [])
    1.20    | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
    1.21  and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) = 
    1.22 -    distinct (flat (map (try_rew thy ro erls subst f) rules))
    1.23 +    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.24    | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 
    1.25 -    distinct (flat (map (try_rew thy ro erls subst f) rules))
    1.26 +    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
    1.27    | filter_appl_rews thy subst f (Rrls _) = [];
    1.28  
    1.29  (*. decide if a tactic is applicable to a given formula; 
    1.30      in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
    1.31 -(* val 
    1.32 -   *)
    1.33  fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
    1.34      try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
    1.35 -  | atomic_appl_tacs thy ro erls f (Rewrite (thm'' as (thmID, _))) =
    1.36 -    try_rew thy (ro, assoc_rew_ord ro) erls [] f 
    1.37 -	    (Thm (thmID, assoc_thm'' thy thm''))
    1.38 -  | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'' as (thmID, _))) =
    1.39 -    try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f 
    1.40 -	    (Thm (thmID, assoc_thm'' thy thm''))
    1.41 +  | atomic_appl_tacs thy ro erls f (Rewrite thm'') =
    1.42 +    try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')
    1.43 +  | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'')) =
    1.44 +    try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f (Thm thm'')
    1.45  
    1.46    | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
    1.47      filter_appl_rews thy [] f (assoc_rls rls')
    1.48 @@ -637,7 +633,7 @@
    1.49  fun guh2rewtac (guh:guh) ([] : subs) =
    1.50      let val [isa, thy, sect, xstr] = guh2theID guh
    1.51      in case sect of
    1.52 -	   "Theorems" => Rewrite (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term))
    1.53 +	   "Theorems" => Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
    1.54  	 | "Rulesets" => Rewrite_Set xstr
    1.55  	 | str => error ("guh2rewtac: not impl. for '"^xstr^"'") 
    1.56      end
    1.57 @@ -645,7 +641,7 @@
    1.58      let val [isa, thy, sect, xstr] = guh2theID guh
    1.59      in case sect of
    1.60          "Theorems" => 
    1.61 -          Rewrite_Inst (subs, (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term)))
    1.62 +          Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
    1.63        | "Rulesets" => Rewrite_Set_Inst (subs,  xstr)
    1.64        | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 
    1.65      end;