changeset 43333 | 2bdec7f430d3 |
parent 43324 | 2b47822868e4 |
child 43596 | 78211f66cf8d |
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 09 22:25:25 2011 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu Jun 09 23:12:02 2011 +0200 @@ -493,7 +493,7 @@ The name "x.1" comes from the "RS spec" !*) val inst = case elem_frees of [_] => I - | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)), + | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)), cterm_of thy1 elem_tuple)]); (*strip quantifier and the implication*)