220 "----------- Pattern.match ------------------------------"; |
220 "----------- Pattern.match ------------------------------"; |
221 val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; |
221 val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; |
222 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; |
222 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; |
223 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) |
223 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) |
224 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty); |
224 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty); |
225 print_depth 999; insts; |
225 print_depth 3; (*999*) insts; |
226 (*val insts = |
226 (*val insts = |
227 ({}, |
227 ({}, |
228 {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))), |
228 {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))), |
229 (("b", 0), ("RealDef.real", Free ("x", "RealDef.real"))), |
229 (("b", 0), ("RealDef.real", Free ("x", "RealDef.real"))), |
230 (("c", 0), ("RealDef.real", Free ("1", "RealDef.real")))})*) |
230 (("c", 0), ("RealDef.real", Free ("1", "RealDef.real")))})*) |