1.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Aug 06 10:38:11 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Aug 06 16:19:30 2012 +0200
     1.3 @@ -769,6 +769,23 @@
     1.4              end
     1.5        end
     1.6  
     1.7 +(* fetch errpatIDs from an arbitrary tactic *)
     1.8 +fun fetchErrorpatterns tac =
     1.9 +  let
    1.10 +    val rlsID =
    1.11 +      case tac of
    1.12 +        Rewrite_Set rlsID => rlsID
    1.13 +      | Rewrite_Set_Inst (_, rlsID) => rlsID
    1.14 +      | _ => "list_rls" (*WN120806 "e_rls" is appropriate, but raises exn 'get_pbt not found: ?!?*)
    1.15 +    val (part, thyID) = thy_containing_rls "Isac" rlsID;
    1.16 +    val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
    1.17 +  in case rls of
    1.18 +        Rls {errpatts, ...} => errpatts
    1.19 +      | Seq {errpatts, ...} => errpatts
    1.20 +      | Rrls {errpatts, ...} => errpatts
    1.21 +      | Erls => []
    1.22 +  end
    1.23 +
    1.24  (*------------------------------------------------------------------(**)
    1.25  end
    1.26  open inform;