equal
deleted
inserted
replaced
127 val ruleN = "rule"; |
127 val ruleN = "rule"; |
128 |
128 |
129 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
129 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
130 |
130 |
131 val def_inst = |
131 val def_inst = |
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: " ^ Syntax.string_of_term (Context.proof_of ctxt) t)); |
137 error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t)); |