equal
deleted
inserted
replaced
46 fn Const ("Nominal.perm", _) $ _ $ t => |
46 fn Const ("Nominal.perm", _) $ _ $ t => |
47 if the_default "" (try (head_of #> dest_Const #> fst) t) mem names |
47 if the_default "" (try (head_of #> dest_Const #> fst) t) mem names |
48 then SOME perm_bool else NONE |
48 then SOME perm_bool else NONE |
49 | _ => NONE); |
49 | _ => NONE); |
50 |
50 |
51 val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; |
51 val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE; |
52 |
52 |
53 fun transp ([] :: _) = [] |
53 fun transp ([] :: _) = [] |
54 | transp xs = map hd xs :: transp (map tl xs); |
54 | transp xs = map hd xs :: transp (map tl xs); |
55 |
55 |
56 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of |
56 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of |