1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed May 16 08:59:09 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed May 16 15:01:47 2012 +0200
     1.3 @@ -631,17 +631,6 @@
     1.4  		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end
     1.5    end;
     1.6  
     1.7 -(* error patterns and fill patterns *)
     1.8 -type errpatID = string
     1.9 -type fillpatID = string
    1.10 -type errpat =
    1.11 -  errpatID    (* one identifier for a list of patterns *)
    1.12 -  * term list (* error patterns                        *)
    1.13 -  * thm list  (* thms related to error patterns;
    1.14 -                 note that respective lhs do not match
    1.15 -                 (which reflects student's error)      *)
    1.16 -val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
    1.17 -
    1.18  (* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
    1.19  fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
    1.20    let