src/Pure/Isar/expression.ML
changeset 49749 f27c96e98672
parent 47315 89a4bbf9790d
child 49817 85b37aece3b3
equal deleted inserted replaced
49748:a346daa8a1f4 49749:f27c96e98672
   525     val _ = Local_Defs.cert_def ctxt eq;
   525     val _ = Local_Defs.cert_def ctxt eq;
   526     val ((y, T), b) = Local_Defs.abs_def eq;
   526     val ((y, T), b) = Local_Defs.abs_def eq;
   527     val b' = norm_term env b;
   527     val b' = norm_term env b;
   528     fun err msg = error (msg ^ ": " ^ quote y);
   528     fun err msg = error (msg ^ ": " ^ quote y);
   529   in
   529   in
   530     case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
   530     (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
   531       [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |
   531       [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
   532       dups => if forall (fn (_, b'') => b' aconv b'') dups
   532     | dups =>
   533         then (xs, env, eqs)
   533         if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
   534         else err "Attempt to redefine variable"
   534         else err "Attempt to redefine variable")
   535   end;
   535   end;
   536 
   536 
   537 (* text has the following structure:
   537 (* text has the following structure:
   538        (((exts, exts'), (ints, ints')), (xs, env, defs))
   538        (((exts, exts'), (ints, ints')), (xs, env, defs))
   539    where
   539    where