src/Provers/hypsubst.ML
 changeset 21227 76d6d445d69b parent 21221 ef30d1e6f03a child 21588 cd0dc678a205
equal inserted replaced
21226:a607ae87ee81 21227:76d6d445d69b
`   107 fun eq_var bnd novars =`
`   107 fun eq_var bnd novars =`
`   108   let fun eq_var_aux k (Const("all",_) \$ Abs(_,_,t)) = eq_var_aux k t`
`   108   let fun eq_var_aux k (Const("all",_) \$ Abs(_,_,t)) = eq_var_aux k t`
`   109         | eq_var_aux k (Const("==>",_) \$ A \$ B) =`
`   109         | eq_var_aux k (Const("==>",_) \$ A \$ B) =`
`   110               ((k, inspect_pair bnd novars`
`   110               ((k, inspect_pair bnd novars`
`   111                     (Data.dest_eq (Data.dest_Trueprop A)))`
`   111                     (Data.dest_eq (Data.dest_Trueprop A)))`
`   112                       (*Exception comes from inspect_pair or dest_eq*)`
`   112                handle TERM _ => eq_var_aux (k+1) B`
`   113                handle _ => eq_var_aux (k+1) B)`
`   113                  | Match => eq_var_aux (k+1) B)`
`   114         | eq_var_aux k _ = raise EQ_VAR`
`   114         | eq_var_aux k _ = raise EQ_VAR`
`   115   in  eq_var_aux 0  end;`
`   115   in  eq_var_aux 0  end;`
`   116 `
`   116 `
`   117 (*For the simpset.  Adds ALL suitable equalities, even if not first!`
`   117 (*For the simpset.  Adds ALL suitable equalities, even if not first!`
`   118   No vars are allowed here, as simpsets are built from meta-assumptions*)`
`   118   No vars are allowed here, as simpsets are built from meta-assumptions*)`
`   119 fun mk_eqs bnd th =`
`   119 fun mk_eqs bnd th =`
`   120     [ if inspect_pair bnd false (Data.dest_eq`
`   120     [ if inspect_pair bnd false (Data.dest_eq`
`   121                                    (Data.dest_Trueprop (#prop (rep_thm th))))`
`   121                                    (Data.dest_Trueprop (#prop (rep_thm th))))`
`   122       then th RS Data.eq_reflection`
`   122       then th RS Data.eq_reflection`
`   123       else symmetric(th RS Data.eq_reflection) (*reorient*) ]`
`   123       else symmetric(th RS Data.eq_reflection) (*reorient*) ]`
`   124     handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)`
`   124     handle TERM _ => [] | Match => [];`
`   125 `
`   125 `
`   126 local`
`   126 local`
`   127 in`
`   127 in`
`   128 `
`   128 `
`   129   (*Select a suitable equality assumption; substitute throughout the subgoal`
`   129   (*Select a suitable equality assumption; substitute throughout the subgoal`