src/Pure/tactic.ML
changeset 17271 2756a73f63a5
parent 17203 29b2563f5c11
child 17496 26535df536ae
     1.1 --- a/src/Pure/tactic.ML	Tue Sep 06 08:29:17 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Sep 06 08:30:43 2005 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4    let val thy = Thm.theory_of_thm st
     1.5        and params = params_of_state st i
     1.6        and rts = types_sorts rule and (types,sorts) = types_sorts st
     1.7 -      fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm)
     1.8 +      fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
     1.9          | types' ixn = types ixn;
    1.10        val used = Drule.add_used rule (Drule.add_used st []);
    1.11    in read_insts thy rts (types',sorts) used sinsts end;
    1.12 @@ -666,7 +666,7 @@
    1.13      val frees = map Term.dest_Free (Term.term_frees statement);
    1.14      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.15      val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    1.16 -    val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    1.17 +    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    1.18  
    1.19      fun err msg = raise ERROR_MESSAGE
    1.20        (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^