changeset 60642 | 48dd1cefb4ae |
parent 60552 | 742b553d88b2 |
child 60653 | 7df8e5b05f5a |
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jul 05 15:02:30 2015 +0200 @@ -57,7 +57,7 @@ fun add_inst (xi, t) (Ts, ts) = (case AList.lookup (op =) tyvars xi of - SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts) + SOME S => (((xi, S), certT (Logic.dest_type t)) :: Ts, ts) | NONE => (case AList.lookup (op =) tvars xi of SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts)