52 val T2 = case z of Free(_, T) => T |
52 val T2 = case z of Free(_, T) => T |
53 | Const ("Pair", Type ("fun", [_, Type |
53 | Const ("Pair", Type ("fun", [_, Type |
54 ("fun", [_, T])])) $ _ $ _ => T; |
54 ("fun", [_, T])])) $ _ $ _ => T; |
55 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end; |
55 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end; |
56 |
56 |
57 fun dest_Goal (Const ("Goal", _) $ P) = P; |
|
58 |
|
59 (** maps a goal of the form: |
57 (** maps a goal of the form: |
60 1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) |
58 1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) |
61 fun get_vars thm = let val c = dest_Goal (concl_of (thm)); |
59 fun get_vars thm = let val c = Logic.unprotect (concl_of (thm)); |
62 val d = Logic.strip_assums_concl c; |
60 val d = Logic.strip_assums_concl c; |
63 val Const _ $ pre $ _ $ _ = dest_Trueprop d; |
61 val Const _ $ pre $ _ $ _ = dest_Trueprop d; |
64 in mk_vars pre end; |
62 in mk_vars pre end; |
65 |
63 |
66 |
64 |