1.1 --- a/src/Tools/isac/Interpret/inform.sml	Fri May 25 09:58:20 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Fri May 25 16:30:15 2012 +0200
     1.3 @@ -745,6 +745,30 @@
     1.4        |> flat
     1.5    in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
     1.6  
     1.7 +(* check if an input formula is exactly equal the rewrite from a rule
     1.8 +   which is stored at the pos where the input is stored of "ok". *)
     1.9 +fun is_exactly_equal (pt, pos as (p, _)) istr =
    1.10 +  case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
    1.11 +    NONE => ("syntax error in '" ^ istr ^ "'", Tac "")
    1.12 +  | SOME ifo => 
    1.13 +      let
    1.14 +        val p' = lev_on p;
    1.15 +        val tac = get_obj g_tac pt p';
    1.16 +      in 
    1.17 +        case applicable_in pos pt tac of
    1.18 +          Notappl msg => (msg, Tac "")
    1.19 +        | Appl rew =>
    1.20 +            let
    1.21 +              val res = case rew of
    1.22 +                  Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
    1.23 +                | Rewrite' (_, _, _, _, _, _, (res, _)) => res
    1.24 +            in 
    1.25 +              if not (ifo = res)
    1.26 +              then ("input does not exactly fill the gaps", Tac "")
    1.27 +              else ("ok", tac)
    1.28 +            end
    1.29 +      end
    1.30 +
    1.31  (*------------------------------------------------------------------(**)
    1.32  end
    1.33  open inform;