equal
deleted
inserted
replaced
142 val setT = Term.fastype_of set; |
142 val setT = Term.fastype_of set; |
143 val oldT = HOLogic.dest_setT setT handle TYPE _ => |
143 val oldT = HOLogic.dest_setT setT handle TYPE _ => |
144 error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT)); |
144 error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT)); |
145 |
145 |
146 val goal = mk_inhabited set; |
146 val goal = mk_inhabited set; |
147 val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT)); |
147 val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT)); |
148 |
148 |
149 |
149 |
150 (* lhs *) |
150 (* lhs *) |
151 |
151 |
152 val args = map (ProofContext.check_tfree tmp_ctxt') raw_args; |
152 val args = map (ProofContext.check_tfree tmp_ctxt') raw_args; |