equal
deleted
inserted
replaced
132 ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
132 ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
133 -- Args.term) >> SOME || |
133 -- Args.term) >> SOME || |
134 inst >> Option.map (pair NONE); |
134 inst >> Option.map (pair NONE); |
135 |
135 |
136 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
136 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
137 error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t)); |
137 error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t)); |
138 |
138 |
139 fun unless_more_args scan = Scan.unless (Scan.lift |
139 fun unless_more_args scan = Scan.unless (Scan.lift |
140 ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan; |
140 ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan; |
141 |
141 |
142 |
142 |