equal
deleted
inserted
replaced
381 |
381 |
382 fun singl x = ConsC $ x $ NilC; |
382 fun singl x = ConsC $ x $ NilC; |
383 |
383 |
384 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) |
384 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) |
385 let |
385 let |
386 val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); |
386 (* FIXME proper name context!? *) |
|
387 val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT); |
387 val e = if opti then singl e else e; |
388 val e = if opti then singl e else e; |
388 val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e; |
389 val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e; |
389 val case2 = |
390 val case2 = |
390 Syntax.const @{syntax_const "_case1"} $ |
391 Syntax.const @{syntax_const "_case1"} $ |
391 Syntax.const @{const_syntax dummy_pattern} $ NilC; |
392 Syntax.const @{const_syntax dummy_pattern} $ NilC; |